(0) Obligation:
Clauses:
delete(X, tree(X, void, Right), Right).
delete(X, tree(X, Left, void), Left).
delete(X, tree(X, Left, Right), tree(Y, Left, Right1)) :- delmin(Right, Y, Right1).
delete(X, tree(Y, Left, Right), tree(Y, Left1, Right)) :- ','(less(X, Y), delete(X, Left, Left1)).
delete(X, tree(Y, Left, Right), tree(Y, Left, Right1)) :- ','(less(Y, X), delete(X, Right, Right1)).
delmin(tree(Y, void, Right), Y, Right).
delmin(tree(X, Left, X1), Y, tree(X, Left1, X2)) :- delmin(Left, Y, Left1).
less(0, s(X3)).
less(s(X), s(Y)) :- less(X, Y).
Query: delete(a,g,a)
(1) PrologToDTProblemTransformerProof (SOUND transformation)
Built DT problem from termination graph DT10.
(2) Obligation:
Triples:
lessA(s(X1), s(X2)) :- lessA(X1, X2).
lessF(s(X1), s(X2)) :- lessF(X1, X2).
pD(X1, X2, X3) :- lessF(X1, X2).
pD(X1, X2, X3) :- ','(lesscF(X1, X2), deleteB(X2, void, X3)).
delminG(tree(X1, X2, X3), X4, tree(X1, X5, X6)) :- delminG(X2, X4, X5).
pC(X1, X2, X3) :- lessA(X1, X2).
pC(X1, X2, X3) :- ','(lesscA(X1, X2), deleteE(X1, X3)).
pH(X1, X2, X3, X4) :- lessF(X1, X2).
pH(X1, X2, X3, X4) :- ','(lesscF(X1, X2), deleteB(X2, X3, X4)).
lessM(s(X1), s(X2)) :- lessM(X1, X2).
pI(X1, X2, X3, X4) :- lessM(X1, X2).
pI(X1, X2, X3, X4) :- ','(lesscM(X1, X2), deleteK(X1, X3, X4)).
deleteK(X1, tree(X1, X2, X3), tree(X4, X2, X5)) :- delminG(X3, X4, X5).
deleteK(X1, tree(X2, X3, X4), tree(X2, X5, X4)) :- pI(X1, X2, X3, X5).
deleteK(X1, tree(X2, X3, X4), tree(X2, X3, X5)) :- pJ(X2, X1, X4, X5).
pJ(X1, X2, X3, X4) :- lessM(X1, X2).
pJ(X1, X2, X3, X4) :- ','(lesscM(X1, X2), deleteK(X2, X3, X4)).
pL(X1, X2, X3, X4) :- lessF(X1, X2).
pL(X1, X2, X3, X4) :- ','(lesscF(X1, X2), deleteB(X2, X3, X4)).
deleteB(X1, tree(X2, void, void), tree(X2, X3, void)) :- pC(X1, X2, X3).
deleteB(X1, tree(X2, void, void), tree(X2, void, X3)) :- pD(X2, X1, X3).
deleteB(0, tree(s(X1), void, void), tree(s(X1), X2, void)) :- deleteE(0, X2).
deleteB(s(X1), tree(s(X2), void, void), tree(s(X2), X3, void)) :- lessA(X1, X2).
deleteB(s(X1), tree(s(X2), void, void), tree(s(X2), X3, void)) :- ','(lesscA(X1, X2), deleteE(s(X1), X3)).
deleteB(X1, tree(X2, void, void), tree(X2, void, X3)) :- pD(X2, X1, X3).
deleteB(s(X1), tree(0, void, void), tree(0, void, X2)) :- deleteB(s(X1), void, X2).
deleteB(s(X1), tree(s(X2), void, void), tree(s(X2), void, X3)) :- lessF(X2, X1).
deleteB(s(X1), tree(s(X2), void, void), tree(s(X2), void, X3)) :- ','(lesscF(X2, X1), deleteB(s(X1), void, X3)).
deleteB(X1, tree(X1, void, tree(X2, X3, X4)), tree(X5, void, tree(X2, X6, X7))) :- delminG(X3, X5, X6).
deleteB(X1, tree(X2, void, X3), tree(X2, X4, X3)) :- pC(X1, X2, X4).
deleteB(X1, tree(X2, void, X3), tree(X2, void, X4)) :- pH(X2, X1, X3, X4).
deleteB(0, tree(s(X1), void, X2), tree(s(X1), X3, X2)) :- deleteE(0, X3).
deleteB(s(X1), tree(s(X2), void, X3), tree(s(X2), X4, X3)) :- lessA(X1, X2).
deleteB(s(X1), tree(s(X2), void, X3), tree(s(X2), X4, X3)) :- ','(lesscA(X1, X2), deleteE(s(X1), X4)).
deleteB(X1, tree(X2, void, X3), tree(X2, void, X4)) :- pH(X2, X1, X3, X4).
deleteB(s(X1), tree(0, void, X2), tree(0, void, X3)) :- deleteB(s(X1), X2, X3).
deleteB(s(X1), tree(s(X2), void, X3), tree(s(X2), void, X4)) :- lessF(X2, X1).
deleteB(s(X1), tree(s(X2), void, X3), tree(s(X2), void, X4)) :- ','(lesscF(X2, X1), deleteB(s(X1), X3, X4)).
deleteB(X1, tree(X2, X3, void), tree(X2, X4, void)) :- lessA(X1, X2).
deleteB(X1, tree(X2, tree(X1, X3, X4), void), tree(X2, tree(X5, X3, X6), void)) :- ','(lesscA(X1, X2), delminG(X4, X5, X6)).
deleteB(X1, tree(X2, tree(X3, X4, X5), void), tree(X2, tree(X3, X6, X5), void)) :- ','(lesscA(X1, X2), pI(X1, X3, X4, X6)).
deleteB(X1, tree(X2, tree(X3, X4, X5), void), tree(X2, tree(X3, X4, X6), void)) :- ','(lesscA(X1, X2), pJ(X3, X1, X5, X6)).
deleteB(X1, tree(X2, X3, void), tree(X2, X3, X4)) :- pD(X2, X1, X4).
deleteB(0, tree(s(X1), X2, void), tree(s(X1), X3, void)) :- deleteK(0, X2, X3).
deleteB(s(X1), tree(s(X2), X3, void), tree(s(X2), X4, void)) :- lessA(X1, X2).
deleteB(s(X1), tree(s(X2), X3, void), tree(s(X2), X4, void)) :- ','(lesscA(X1, X2), deleteK(s(X1), X3, X4)).
deleteB(X1, tree(X2, X3, void), tree(X2, X3, X4)) :- pD(X2, X1, X4).
deleteB(s(X1), tree(0, X2, void), tree(0, X2, X3)) :- deleteB(s(X1), void, X3).
deleteB(s(X1), tree(s(X2), X3, void), tree(s(X2), X3, X4)) :- lessF(X2, X1).
deleteB(s(X1), tree(s(X2), X3, void), tree(s(X2), X3, X4)) :- ','(lesscF(X2, X1), deleteB(s(X1), void, X4)).
deleteB(X1, tree(X1, X2, tree(X3, X4, X5)), tree(X6, X2, tree(X3, X7, X8))) :- delminG(X4, X6, X7).
deleteB(X1, tree(X2, X3, X4), tree(X2, X5, X4)) :- lessA(X1, X2).
deleteB(X1, tree(X2, X3, X4), tree(X2, X5, X4)) :- ','(lesscA(X1, X2), deleteK(X1, X3, X5)).
deleteB(X1, tree(X2, X3, X4), tree(X2, X3, X5)) :- pL(X2, X1, X4, X5).
deleteB(0, tree(s(X1), X2, X3), tree(s(X1), X4, X3)) :- deleteK(0, X2, X4).
deleteB(s(X1), tree(s(X2), X3, X4), tree(s(X2), X5, X4)) :- lessA(X1, X2).
deleteB(s(X1), tree(s(X2), X3, X4), tree(s(X2), X5, X4)) :- ','(lesscA(X1, X2), deleteK(s(X1), X3, X5)).
deleteB(X1, tree(X2, X3, X4), tree(X2, X3, X5)) :- pL(X2, X1, X4, X5).
deleteB(s(X1), tree(0, X2, X3), tree(0, X2, X4)) :- deleteB(s(X1), X3, X4).
deleteB(s(X1), tree(s(X2), X3, X4), tree(s(X2), X3, X5)) :- lessF(X2, X1).
deleteB(s(X1), tree(s(X2), X3, X4), tree(s(X2), X3, X5)) :- ','(lesscF(X2, X1), deleteB(s(X1), X4, X5)).
Clauses:
lesscA(0, s(X1)).
lesscA(s(X1), s(X2)) :- lesscA(X1, X2).
deletecB(X1, tree(X1, void, X2), X2).
deletecB(X1, tree(X1, void, void), void).
deletecB(X1, tree(X2, void, void), tree(X2, X3, void)) :- qcC(X1, X2, X3).
deletecB(X1, tree(X2, void, void), tree(X2, void, X3)) :- qcD(X2, X1, X3).
deletecB(0, tree(s(X1), void, void), tree(s(X1), X2, void)) :- deletecE(0, X2).
deletecB(s(X1), tree(s(X2), void, void), tree(s(X2), X3, void)) :- ','(lesscA(X1, X2), deletecE(s(X1), X3)).
deletecB(X1, tree(X2, void, void), tree(X2, void, X3)) :- qcD(X2, X1, X3).
deletecB(s(X1), tree(0, void, void), tree(0, void, X2)) :- deletecB(s(X1), void, X2).
deletecB(s(X1), tree(s(X2), void, void), tree(s(X2), void, X3)) :- ','(lesscF(X2, X1), deletecB(s(X1), void, X3)).
deletecB(X1, tree(X1, void, tree(X2, void, X3)), tree(X2, void, X3)).
deletecB(X1, tree(X1, void, tree(X2, X3, X4)), tree(X5, void, tree(X2, X6, X7))) :- delmincG(X3, X5, X6).
deletecB(X1, tree(X2, void, X3), tree(X2, X4, X3)) :- qcC(X1, X2, X4).
deletecB(X1, tree(X2, void, X3), tree(X2, void, X4)) :- qcH(X2, X1, X3, X4).
deletecB(0, tree(s(X1), void, X2), tree(s(X1), X3, X2)) :- deletecE(0, X3).
deletecB(s(X1), tree(s(X2), void, X3), tree(s(X2), X4, X3)) :- ','(lesscA(X1, X2), deletecE(s(X1), X4)).
deletecB(X1, tree(X2, void, X3), tree(X2, void, X4)) :- qcH(X2, X1, X3, X4).
deletecB(s(X1), tree(0, void, X2), tree(0, void, X3)) :- deletecB(s(X1), X2, X3).
deletecB(s(X1), tree(s(X2), void, X3), tree(s(X2), void, X4)) :- ','(lesscF(X2, X1), deletecB(s(X1), X3, X4)).
deletecB(X1, tree(X1, X2, void), X2).
deletecB(X1, tree(X2, tree(X1, void, X3), void), tree(X2, X3, void)) :- lesscA(X1, X2).
deletecB(X1, tree(X2, tree(X1, X3, void), void), tree(X2, X3, void)) :- lesscA(X1, X2).
deletecB(X1, tree(X2, tree(X1, X3, X4), void), tree(X2, tree(X5, X3, X6), void)) :- ','(lesscA(X1, X2), delmincG(X4, X5, X6)).
deletecB(X1, tree(X2, tree(X3, X4, X5), void), tree(X2, tree(X3, X6, X5), void)) :- ','(lesscA(X1, X2), qcI(X1, X3, X4, X6)).
deletecB(X1, tree(X2, tree(X3, X4, X5), void), tree(X2, tree(X3, X4, X6), void)) :- ','(lesscA(X1, X2), qcJ(X3, X1, X5, X6)).
deletecB(X1, tree(X2, X3, void), tree(X2, X3, X4)) :- qcD(X2, X1, X4).
deletecB(0, tree(s(X1), X2, void), tree(s(X1), X3, void)) :- deletecK(0, X2, X3).
deletecB(s(X1), tree(s(X2), X3, void), tree(s(X2), X4, void)) :- ','(lesscA(X1, X2), deletecK(s(X1), X3, X4)).
deletecB(X1, tree(X2, X3, void), tree(X2, X3, X4)) :- qcD(X2, X1, X4).
deletecB(s(X1), tree(0, X2, void), tree(0, X2, X3)) :- deletecB(s(X1), void, X3).
deletecB(s(X1), tree(s(X2), X3, void), tree(s(X2), X3, X4)) :- ','(lesscF(X2, X1), deletecB(s(X1), void, X4)).
deletecB(X1, tree(X1, X2, tree(X3, void, X4)), tree(X3, X2, X4)).
deletecB(X1, tree(X1, X2, tree(X3, X4, X5)), tree(X6, X2, tree(X3, X7, X8))) :- delmincG(X4, X6, X7).
deletecB(X1, tree(X2, X3, X4), tree(X2, X5, X4)) :- ','(lesscA(X1, X2), deletecK(X1, X3, X5)).
deletecB(X1, tree(X2, X3, X4), tree(X2, X3, X5)) :- qcL(X2, X1, X4, X5).
deletecB(0, tree(s(X1), X2, X3), tree(s(X1), X4, X3)) :- deletecK(0, X2, X4).
deletecB(s(X1), tree(s(X2), X3, X4), tree(s(X2), X5, X4)) :- ','(lesscA(X1, X2), deletecK(s(X1), X3, X5)).
deletecB(X1, tree(X2, X3, X4), tree(X2, X3, X5)) :- qcL(X2, X1, X4, X5).
deletecB(s(X1), tree(0, X2, X3), tree(0, X2, X4)) :- deletecB(s(X1), X3, X4).
deletecB(s(X1), tree(s(X2), X3, X4), tree(s(X2), X3, X5)) :- ','(lesscF(X2, X1), deletecB(s(X1), X4, X5)).
lesscF(0, s(X1)).
lesscF(s(X1), s(X2)) :- lesscF(X1, X2).
qcD(X1, X2, X3) :- ','(lesscF(X1, X2), deletecB(X2, void, X3)).
delmincG(tree(X1, void, X2), X1, X2).
delmincG(tree(X1, X2, X3), X4, tree(X1, X5, X6)) :- delmincG(X2, X4, X5).
qcC(X1, X2, X3) :- ','(lesscA(X1, X2), deletecE(X1, X3)).
qcH(X1, X2, X3, X4) :- ','(lesscF(X1, X2), deletecB(X2, X3, X4)).
lesscM(0, s(X1)).
lesscM(s(X1), s(X2)) :- lesscM(X1, X2).
qcI(X1, X2, X3, X4) :- ','(lesscM(X1, X2), deletecK(X1, X3, X4)).
deletecK(X1, tree(X1, void, X2), X2).
deletecK(X1, tree(X1, X2, void), X2).
deletecK(X1, tree(X1, X2, X3), tree(X4, X2, X5)) :- delmincG(X3, X4, X5).
deletecK(X1, tree(X2, X3, X4), tree(X2, X5, X4)) :- qcI(X1, X2, X3, X5).
deletecK(X1, tree(X2, X3, X4), tree(X2, X3, X5)) :- qcJ(X2, X1, X4, X5).
qcJ(X1, X2, X3, X4) :- ','(lesscM(X1, X2), deletecK(X2, X3, X4)).
qcL(X1, X2, X3, X4) :- ','(lesscF(X1, X2), deletecB(X2, X3, X4)).
Afs:
deleteB(x1, x2, x3) = deleteB(x2)
(3) UndefinedPredicateInTriplesTransformerProof (SOUND transformation)
Deleted triples and predicates having undefined goals [DT09].
(4) Obligation:
Triples:
lessA(s(X1), s(X2)) :- lessA(X1, X2).
lessF(s(X1), s(X2)) :- lessF(X1, X2).
pD(X1, X2, X3) :- lessF(X1, X2).
pD(X1, X2, X3) :- ','(lesscF(X1, X2), deleteB(X2, void, X3)).
delminG(tree(X1, X2, X3), X4, tree(X1, X5, X6)) :- delminG(X2, X4, X5).
pC(X1, X2, X3) :- lessA(X1, X2).
pH(X1, X2, X3, X4) :- lessF(X1, X2).
pH(X1, X2, X3, X4) :- ','(lesscF(X1, X2), deleteB(X2, X3, X4)).
lessM(s(X1), s(X2)) :- lessM(X1, X2).
pI(X1, X2, X3, X4) :- lessM(X1, X2).
pI(X1, X2, X3, X4) :- ','(lesscM(X1, X2), deleteK(X1, X3, X4)).
deleteK(X1, tree(X1, X2, X3), tree(X4, X2, X5)) :- delminG(X3, X4, X5).
deleteK(X1, tree(X2, X3, X4), tree(X2, X5, X4)) :- pI(X1, X2, X3, X5).
deleteK(X1, tree(X2, X3, X4), tree(X2, X3, X5)) :- pJ(X2, X1, X4, X5).
pJ(X1, X2, X3, X4) :- lessM(X1, X2).
pJ(X1, X2, X3, X4) :- ','(lesscM(X1, X2), deleteK(X2, X3, X4)).
pL(X1, X2, X3, X4) :- lessF(X1, X2).
pL(X1, X2, X3, X4) :- ','(lesscF(X1, X2), deleteB(X2, X3, X4)).
deleteB(X1, tree(X2, void, void), tree(X2, X3, void)) :- pC(X1, X2, X3).
deleteB(X1, tree(X2, void, void), tree(X2, void, X3)) :- pD(X2, X1, X3).
deleteB(s(X1), tree(s(X2), void, void), tree(s(X2), X3, void)) :- lessA(X1, X2).
deleteB(X1, tree(X2, void, void), tree(X2, void, X3)) :- pD(X2, X1, X3).
deleteB(s(X1), tree(0, void, void), tree(0, void, X2)) :- deleteB(s(X1), void, X2).
deleteB(s(X1), tree(s(X2), void, void), tree(s(X2), void, X3)) :- lessF(X2, X1).
deleteB(s(X1), tree(s(X2), void, void), tree(s(X2), void, X3)) :- ','(lesscF(X2, X1), deleteB(s(X1), void, X3)).
deleteB(X1, tree(X1, void, tree(X2, X3, X4)), tree(X5, void, tree(X2, X6, X7))) :- delminG(X3, X5, X6).
deleteB(X1, tree(X2, void, X3), tree(X2, X4, X3)) :- pC(X1, X2, X4).
deleteB(X1, tree(X2, void, X3), tree(X2, void, X4)) :- pH(X2, X1, X3, X4).
deleteB(s(X1), tree(s(X2), void, X3), tree(s(X2), X4, X3)) :- lessA(X1, X2).
deleteB(X1, tree(X2, void, X3), tree(X2, void, X4)) :- pH(X2, X1, X3, X4).
deleteB(s(X1), tree(0, void, X2), tree(0, void, X3)) :- deleteB(s(X1), X2, X3).
deleteB(s(X1), tree(s(X2), void, X3), tree(s(X2), void, X4)) :- lessF(X2, X1).
deleteB(s(X1), tree(s(X2), void, X3), tree(s(X2), void, X4)) :- ','(lesscF(X2, X1), deleteB(s(X1), X3, X4)).
deleteB(X1, tree(X2, X3, void), tree(X2, X4, void)) :- lessA(X1, X2).
deleteB(X1, tree(X2, tree(X1, X3, X4), void), tree(X2, tree(X5, X3, X6), void)) :- ','(lesscA(X1, X2), delminG(X4, X5, X6)).
deleteB(X1, tree(X2, tree(X3, X4, X5), void), tree(X2, tree(X3, X6, X5), void)) :- ','(lesscA(X1, X2), pI(X1, X3, X4, X6)).
deleteB(X1, tree(X2, tree(X3, X4, X5), void), tree(X2, tree(X3, X4, X6), void)) :- ','(lesscA(X1, X2), pJ(X3, X1, X5, X6)).
deleteB(X1, tree(X2, X3, void), tree(X2, X3, X4)) :- pD(X2, X1, X4).
deleteB(0, tree(s(X1), X2, void), tree(s(X1), X3, void)) :- deleteK(0, X2, X3).
deleteB(s(X1), tree(s(X2), X3, void), tree(s(X2), X4, void)) :- lessA(X1, X2).
deleteB(s(X1), tree(s(X2), X3, void), tree(s(X2), X4, void)) :- ','(lesscA(X1, X2), deleteK(s(X1), X3, X4)).
deleteB(X1, tree(X2, X3, void), tree(X2, X3, X4)) :- pD(X2, X1, X4).
deleteB(s(X1), tree(0, X2, void), tree(0, X2, X3)) :- deleteB(s(X1), void, X3).
deleteB(s(X1), tree(s(X2), X3, void), tree(s(X2), X3, X4)) :- lessF(X2, X1).
deleteB(s(X1), tree(s(X2), X3, void), tree(s(X2), X3, X4)) :- ','(lesscF(X2, X1), deleteB(s(X1), void, X4)).
deleteB(X1, tree(X1, X2, tree(X3, X4, X5)), tree(X6, X2, tree(X3, X7, X8))) :- delminG(X4, X6, X7).
deleteB(X1, tree(X2, X3, X4), tree(X2, X5, X4)) :- lessA(X1, X2).
deleteB(X1, tree(X2, X3, X4), tree(X2, X5, X4)) :- ','(lesscA(X1, X2), deleteK(X1, X3, X5)).
deleteB(X1, tree(X2, X3, X4), tree(X2, X3, X5)) :- pL(X2, X1, X4, X5).
deleteB(0, tree(s(X1), X2, X3), tree(s(X1), X4, X3)) :- deleteK(0, X2, X4).
deleteB(s(X1), tree(s(X2), X3, X4), tree(s(X2), X5, X4)) :- lessA(X1, X2).
deleteB(s(X1), tree(s(X2), X3, X4), tree(s(X2), X5, X4)) :- ','(lesscA(X1, X2), deleteK(s(X1), X3, X5)).
deleteB(X1, tree(X2, X3, X4), tree(X2, X3, X5)) :- pL(X2, X1, X4, X5).
deleteB(s(X1), tree(0, X2, X3), tree(0, X2, X4)) :- deleteB(s(X1), X3, X4).
deleteB(s(X1), tree(s(X2), X3, X4), tree(s(X2), X3, X5)) :- lessF(X2, X1).
deleteB(s(X1), tree(s(X2), X3, X4), tree(s(X2), X3, X5)) :- ','(lesscF(X2, X1), deleteB(s(X1), X4, X5)).
Clauses:
lesscA(0, s(X1)).
lesscA(s(X1), s(X2)) :- lesscA(X1, X2).
deletecB(X1, tree(X1, void, X2), X2).
deletecB(X1, tree(X1, void, void), void).
deletecB(X1, tree(X2, void, void), tree(X2, void, X3)) :- qcD(X2, X1, X3).
deletecB(X1, tree(X2, void, void), tree(X2, void, X3)) :- qcD(X2, X1, X3).
deletecB(s(X1), tree(0, void, void), tree(0, void, X2)) :- deletecB(s(X1), void, X2).
deletecB(s(X1), tree(s(X2), void, void), tree(s(X2), void, X3)) :- ','(lesscF(X2, X1), deletecB(s(X1), void, X3)).
deletecB(X1, tree(X1, void, tree(X2, void, X3)), tree(X2, void, X3)).
deletecB(X1, tree(X1, void, tree(X2, X3, X4)), tree(X5, void, tree(X2, X6, X7))) :- delmincG(X3, X5, X6).
deletecB(X1, tree(X2, void, X3), tree(X2, void, X4)) :- qcH(X2, X1, X3, X4).
deletecB(X1, tree(X2, void, X3), tree(X2, void, X4)) :- qcH(X2, X1, X3, X4).
deletecB(s(X1), tree(0, void, X2), tree(0, void, X3)) :- deletecB(s(X1), X2, X3).
deletecB(s(X1), tree(s(X2), void, X3), tree(s(X2), void, X4)) :- ','(lesscF(X2, X1), deletecB(s(X1), X3, X4)).
deletecB(X1, tree(X1, X2, void), X2).
deletecB(X1, tree(X2, tree(X1, void, X3), void), tree(X2, X3, void)) :- lesscA(X1, X2).
deletecB(X1, tree(X2, tree(X1, X3, void), void), tree(X2, X3, void)) :- lesscA(X1, X2).
deletecB(X1, tree(X2, tree(X1, X3, X4), void), tree(X2, tree(X5, X3, X6), void)) :- ','(lesscA(X1, X2), delmincG(X4, X5, X6)).
deletecB(X1, tree(X2, tree(X3, X4, X5), void), tree(X2, tree(X3, X6, X5), void)) :- ','(lesscA(X1, X2), qcI(X1, X3, X4, X6)).
deletecB(X1, tree(X2, tree(X3, X4, X5), void), tree(X2, tree(X3, X4, X6), void)) :- ','(lesscA(X1, X2), qcJ(X3, X1, X5, X6)).
deletecB(X1, tree(X2, X3, void), tree(X2, X3, X4)) :- qcD(X2, X1, X4).
deletecB(0, tree(s(X1), X2, void), tree(s(X1), X3, void)) :- deletecK(0, X2, X3).
deletecB(s(X1), tree(s(X2), X3, void), tree(s(X2), X4, void)) :- ','(lesscA(X1, X2), deletecK(s(X1), X3, X4)).
deletecB(X1, tree(X2, X3, void), tree(X2, X3, X4)) :- qcD(X2, X1, X4).
deletecB(s(X1), tree(0, X2, void), tree(0, X2, X3)) :- deletecB(s(X1), void, X3).
deletecB(s(X1), tree(s(X2), X3, void), tree(s(X2), X3, X4)) :- ','(lesscF(X2, X1), deletecB(s(X1), void, X4)).
deletecB(X1, tree(X1, X2, tree(X3, void, X4)), tree(X3, X2, X4)).
deletecB(X1, tree(X1, X2, tree(X3, X4, X5)), tree(X6, X2, tree(X3, X7, X8))) :- delmincG(X4, X6, X7).
deletecB(X1, tree(X2, X3, X4), tree(X2, X5, X4)) :- ','(lesscA(X1, X2), deletecK(X1, X3, X5)).
deletecB(X1, tree(X2, X3, X4), tree(X2, X3, X5)) :- qcL(X2, X1, X4, X5).
deletecB(0, tree(s(X1), X2, X3), tree(s(X1), X4, X3)) :- deletecK(0, X2, X4).
deletecB(s(X1), tree(s(X2), X3, X4), tree(s(X2), X5, X4)) :- ','(lesscA(X1, X2), deletecK(s(X1), X3, X5)).
deletecB(X1, tree(X2, X3, X4), tree(X2, X3, X5)) :- qcL(X2, X1, X4, X5).
deletecB(s(X1), tree(0, X2, X3), tree(0, X2, X4)) :- deletecB(s(X1), X3, X4).
deletecB(s(X1), tree(s(X2), X3, X4), tree(s(X2), X3, X5)) :- ','(lesscF(X2, X1), deletecB(s(X1), X4, X5)).
lesscF(0, s(X1)).
lesscF(s(X1), s(X2)) :- lesscF(X1, X2).
qcD(X1, X2, X3) :- ','(lesscF(X1, X2), deletecB(X2, void, X3)).
delmincG(tree(X1, void, X2), X1, X2).
delmincG(tree(X1, X2, X3), X4, tree(X1, X5, X6)) :- delmincG(X2, X4, X5).
qcH(X1, X2, X3, X4) :- ','(lesscF(X1, X2), deletecB(X2, X3, X4)).
lesscM(0, s(X1)).
lesscM(s(X1), s(X2)) :- lesscM(X1, X2).
qcI(X1, X2, X3, X4) :- ','(lesscM(X1, X2), deletecK(X1, X3, X4)).
deletecK(X1, tree(X1, void, X2), X2).
deletecK(X1, tree(X1, X2, void), X2).
deletecK(X1, tree(X1, X2, X3), tree(X4, X2, X5)) :- delmincG(X3, X4, X5).
deletecK(X1, tree(X2, X3, X4), tree(X2, X5, X4)) :- qcI(X1, X2, X3, X5).
deletecK(X1, tree(X2, X3, X4), tree(X2, X3, X5)) :- qcJ(X2, X1, X4, X5).
qcJ(X1, X2, X3, X4) :- ','(lesscM(X1, X2), deletecK(X2, X3, X4)).
qcL(X1, X2, X3, X4) :- ','(lesscF(X1, X2), deletecB(X2, X3, X4)).
Afs:
deleteB(x1, x2, x3) = deleteB(x2)
(5) TriplesToPiDPProof (SOUND transformation)
We use the technique of [DT09]. With regard to the inferred argument filtering the predicates were used in the following modes:
deleteB_in: (f,b,f)
pC_in: (f,b,f)
lessA_in: (f,b)
pD_in: (b,f,f)
lessF_in: (b,f)
lesscF_in: (b,f)
delminG_in: (b,f,f)
pH_in: (b,f,b,f)
lesscA_in: (b,b) (f,b)
pI_in: (b,b,b,f)
lessM_in: (b,b)
lesscM_in: (b,b)
deleteK_in: (b,b,f)
pJ_in: (b,b,b,f)
pL_in: (b,f,b,f)
Transforming
TRIPLES into the following
Term Rewriting System:
Pi DP problem:
The TRS P consists of the following rules:
DELETEB_IN_AGA(X1, tree(X2, void, void), tree(X2, X3, void)) → U24_AGA(X1, X2, X3, pC_in_aga(X1, X2, X3))
DELETEB_IN_AGA(X1, tree(X2, void, void), tree(X2, X3, void)) → PC_IN_AGA(X1, X2, X3)
PC_IN_AGA(X1, X2, X3) → U7_AGA(X1, X2, X3, lessA_in_ag(X1, X2))
PC_IN_AGA(X1, X2, X3) → LESSA_IN_AG(X1, X2)
LESSA_IN_AG(s(X1), s(X2)) → U1_AG(X1, X2, lessA_in_ag(X1, X2))
LESSA_IN_AG(s(X1), s(X2)) → LESSA_IN_AG(X1, X2)
DELETEB_IN_AGA(X1, tree(X2, void, void), tree(X2, void, X3)) → U25_AGA(X1, X2, X3, pD_in_gaa(X2, X1, X3))
DELETEB_IN_AGA(X1, tree(X2, void, void), tree(X2, void, X3)) → PD_IN_GAA(X2, X1, X3)
PD_IN_GAA(X1, X2, X3) → U3_GAA(X1, X2, X3, lessF_in_ga(X1, X2))
PD_IN_GAA(X1, X2, X3) → LESSF_IN_GA(X1, X2)
LESSF_IN_GA(s(X1), s(X2)) → U2_GA(X1, X2, lessF_in_ga(X1, X2))
LESSF_IN_GA(s(X1), s(X2)) → LESSF_IN_GA(X1, X2)
PD_IN_GAA(X1, X2, X3) → U4_GAA(X1, X2, X3, lesscF_in_ga(X1, X2))
U4_GAA(X1, X2, X3, lesscF_out_ga(X1, X2)) → U5_GAA(X1, X2, X3, deleteB_in_aga(X2, void, X3))
U4_GAA(X1, X2, X3, lesscF_out_ga(X1, X2)) → DELETEB_IN_AGA(X2, void, X3)
DELETEB_IN_AGA(s(X1), tree(s(X2), void, void), tree(s(X2), X3, void)) → U26_AGA(X1, X2, X3, lessA_in_ag(X1, X2))
DELETEB_IN_AGA(s(X1), tree(s(X2), void, void), tree(s(X2), X3, void)) → LESSA_IN_AG(X1, X2)
DELETEB_IN_AGA(s(X1), tree(0, void, void), tree(0, void, X2)) → U27_AGA(X1, X2, deleteB_in_aga(s(X1), void, X2))
DELETEB_IN_AGA(s(X1), tree(0, void, void), tree(0, void, X2)) → DELETEB_IN_AGA(s(X1), void, X2)
DELETEB_IN_AGA(s(X1), tree(s(X2), void, void), tree(s(X2), void, X3)) → U28_AGA(X1, X2, X3, lessF_in_ga(X2, X1))
DELETEB_IN_AGA(s(X1), tree(s(X2), void, void), tree(s(X2), void, X3)) → LESSF_IN_GA(X2, X1)
DELETEB_IN_AGA(s(X1), tree(s(X2), void, void), tree(s(X2), void, X3)) → U29_AGA(X1, X2, X3, lesscF_in_ga(X2, X1))
U29_AGA(X1, X2, X3, lesscF_out_ga(X2, X1)) → U30_AGA(X1, X2, X3, deleteB_in_aga(s(X1), void, X3))
U29_AGA(X1, X2, X3, lesscF_out_ga(X2, X1)) → DELETEB_IN_AGA(s(X1), void, X3)
DELETEB_IN_AGA(X1, tree(X1, void, tree(X2, X3, X4)), tree(X5, void, tree(X2, X6, X7))) → U31_AGA(X1, X2, X3, X4, X5, X6, X7, delminG_in_gaa(X3, X5, X6))
DELETEB_IN_AGA(X1, tree(X1, void, tree(X2, X3, X4)), tree(X5, void, tree(X2, X6, X7))) → DELMING_IN_GAA(X3, X5, X6)
DELMING_IN_GAA(tree(X1, X2, X3), X4, tree(X1, X5, X6)) → U6_GAA(X1, X2, X3, X4, X5, X6, delminG_in_gaa(X2, X4, X5))
DELMING_IN_GAA(tree(X1, X2, X3), X4, tree(X1, X5, X6)) → DELMING_IN_GAA(X2, X4, X5)
DELETEB_IN_AGA(X1, tree(X2, void, X3), tree(X2, X4, X3)) → U32_AGA(X1, X2, X3, X4, pC_in_aga(X1, X2, X4))
DELETEB_IN_AGA(X1, tree(X2, void, X3), tree(X2, X4, X3)) → PC_IN_AGA(X1, X2, X4)
DELETEB_IN_AGA(X1, tree(X2, void, X3), tree(X2, void, X4)) → U33_AGA(X1, X2, X3, X4, pH_in_gaga(X2, X1, X3, X4))
DELETEB_IN_AGA(X1, tree(X2, void, X3), tree(X2, void, X4)) → PH_IN_GAGA(X2, X1, X3, X4)
PH_IN_GAGA(X1, X2, X3, X4) → U8_GAGA(X1, X2, X3, X4, lessF_in_ga(X1, X2))
PH_IN_GAGA(X1, X2, X3, X4) → LESSF_IN_GA(X1, X2)
PH_IN_GAGA(X1, X2, X3, X4) → U9_GAGA(X1, X2, X3, X4, lesscF_in_ga(X1, X2))
U9_GAGA(X1, X2, X3, X4, lesscF_out_ga(X1, X2)) → U10_GAGA(X1, X2, X3, X4, deleteB_in_aga(X2, X3, X4))
U9_GAGA(X1, X2, X3, X4, lesscF_out_ga(X1, X2)) → DELETEB_IN_AGA(X2, X3, X4)
DELETEB_IN_AGA(s(X1), tree(s(X2), void, X3), tree(s(X2), X4, X3)) → U34_AGA(X1, X2, X3, X4, lessA_in_ag(X1, X2))
DELETEB_IN_AGA(s(X1), tree(s(X2), void, X3), tree(s(X2), X4, X3)) → LESSA_IN_AG(X1, X2)
DELETEB_IN_AGA(s(X1), tree(0, void, X2), tree(0, void, X3)) → U35_AGA(X1, X2, X3, deleteB_in_aga(s(X1), X2, X3))
DELETEB_IN_AGA(s(X1), tree(0, void, X2), tree(0, void, X3)) → DELETEB_IN_AGA(s(X1), X2, X3)
DELETEB_IN_AGA(s(X1), tree(s(X2), void, X3), tree(s(X2), void, X4)) → U36_AGA(X1, X2, X3, X4, lessF_in_ga(X2, X1))
DELETEB_IN_AGA(s(X1), tree(s(X2), void, X3), tree(s(X2), void, X4)) → LESSF_IN_GA(X2, X1)
DELETEB_IN_AGA(s(X1), tree(s(X2), void, X3), tree(s(X2), void, X4)) → U37_AGA(X1, X2, X3, X4, lesscF_in_ga(X2, X1))
U37_AGA(X1, X2, X3, X4, lesscF_out_ga(X2, X1)) → U38_AGA(X1, X2, X3, X4, deleteB_in_aga(s(X1), X3, X4))
U37_AGA(X1, X2, X3, X4, lesscF_out_ga(X2, X1)) → DELETEB_IN_AGA(s(X1), X3, X4)
DELETEB_IN_AGA(X1, tree(X2, X3, void), tree(X2, X4, void)) → U39_AGA(X1, X2, X3, X4, lessA_in_ag(X1, X2))
DELETEB_IN_AGA(X1, tree(X2, X3, void), tree(X2, X4, void)) → LESSA_IN_AG(X1, X2)
DELETEB_IN_AGA(X1, tree(X2, tree(X1, X3, X4), void), tree(X2, tree(X5, X3, X6), void)) → U40_AGA(X1, X2, X3, X4, X5, X6, lesscA_in_gg(X1, X2))
U40_AGA(X1, X2, X3, X4, X5, X6, lesscA_out_gg(X1, X2)) → U41_AGA(X1, X2, X3, X4, X5, X6, delminG_in_gaa(X4, X5, X6))
U40_AGA(X1, X2, X3, X4, X5, X6, lesscA_out_gg(X1, X2)) → DELMING_IN_GAA(X4, X5, X6)
DELETEB_IN_AGA(X1, tree(X2, tree(X3, X4, X5), void), tree(X2, tree(X3, X6, X5), void)) → U42_AGA(X1, X2, X3, X4, X5, X6, lesscA_in_ag(X1, X2))
U42_AGA(X1, X2, X3, X4, X5, X6, lesscA_out_ag(X1, X2)) → U43_AGA(X1, X2, X3, X4, X5, X6, pI_in_ggga(X1, X3, X4, X6))
U42_AGA(X1, X2, X3, X4, X5, X6, lesscA_out_ag(X1, X2)) → PI_IN_GGGA(X1, X3, X4, X6)
PI_IN_GGGA(X1, X2, X3, X4) → U12_GGGA(X1, X2, X3, X4, lessM_in_gg(X1, X2))
PI_IN_GGGA(X1, X2, X3, X4) → LESSM_IN_GG(X1, X2)
LESSM_IN_GG(s(X1), s(X2)) → U11_GG(X1, X2, lessM_in_gg(X1, X2))
LESSM_IN_GG(s(X1), s(X2)) → LESSM_IN_GG(X1, X2)
PI_IN_GGGA(X1, X2, X3, X4) → U13_GGGA(X1, X2, X3, X4, lesscM_in_gg(X1, X2))
U13_GGGA(X1, X2, X3, X4, lesscM_out_gg(X1, X2)) → U14_GGGA(X1, X2, X3, X4, deleteK_in_gga(X1, X3, X4))
U13_GGGA(X1, X2, X3, X4, lesscM_out_gg(X1, X2)) → DELETEK_IN_GGA(X1, X3, X4)
DELETEK_IN_GGA(X1, tree(X1, X2, X3), tree(X4, X2, X5)) → U15_GGA(X1, X2, X3, X4, X5, delminG_in_gaa(X3, X4, X5))
DELETEK_IN_GGA(X1, tree(X1, X2, X3), tree(X4, X2, X5)) → DELMING_IN_GAA(X3, X4, X5)
DELETEK_IN_GGA(X1, tree(X2, X3, X4), tree(X2, X5, X4)) → U16_GGA(X1, X2, X3, X4, X5, pI_in_ggga(X1, X2, X3, X5))
DELETEK_IN_GGA(X1, tree(X2, X3, X4), tree(X2, X5, X4)) → PI_IN_GGGA(X1, X2, X3, X5)
DELETEK_IN_GGA(X1, tree(X2, X3, X4), tree(X2, X3, X5)) → U17_GGA(X1, X2, X3, X4, X5, pJ_in_ggga(X2, X1, X4, X5))
DELETEK_IN_GGA(X1, tree(X2, X3, X4), tree(X2, X3, X5)) → PJ_IN_GGGA(X2, X1, X4, X5)
PJ_IN_GGGA(X1, X2, X3, X4) → U18_GGGA(X1, X2, X3, X4, lessM_in_gg(X1, X2))
PJ_IN_GGGA(X1, X2, X3, X4) → LESSM_IN_GG(X1, X2)
PJ_IN_GGGA(X1, X2, X3, X4) → U19_GGGA(X1, X2, X3, X4, lesscM_in_gg(X1, X2))
U19_GGGA(X1, X2, X3, X4, lesscM_out_gg(X1, X2)) → U20_GGGA(X1, X2, X3, X4, deleteK_in_gga(X2, X3, X4))
U19_GGGA(X1, X2, X3, X4, lesscM_out_gg(X1, X2)) → DELETEK_IN_GGA(X2, X3, X4)
DELETEB_IN_AGA(X1, tree(X2, tree(X3, X4, X5), void), tree(X2, tree(X3, X4, X6), void)) → U44_AGA(X1, X2, X3, X4, X5, X6, lesscA_in_ag(X1, X2))
U44_AGA(X1, X2, X3, X4, X5, X6, lesscA_out_ag(X1, X2)) → U45_AGA(X1, X2, X3, X4, X5, X6, pJ_in_ggga(X3, X1, X5, X6))
U44_AGA(X1, X2, X3, X4, X5, X6, lesscA_out_ag(X1, X2)) → PJ_IN_GGGA(X3, X1, X5, X6)
DELETEB_IN_AGA(X1, tree(X2, X3, void), tree(X2, X3, X4)) → U46_AGA(X1, X2, X3, X4, pD_in_gaa(X2, X1, X4))
DELETEB_IN_AGA(X1, tree(X2, X3, void), tree(X2, X3, X4)) → PD_IN_GAA(X2, X1, X4)
DELETEB_IN_AGA(0, tree(s(X1), X2, void), tree(s(X1), X3, void)) → U47_AGA(X1, X2, X3, deleteK_in_gga(0, X2, X3))
DELETEB_IN_AGA(0, tree(s(X1), X2, void), tree(s(X1), X3, void)) → DELETEK_IN_GGA(0, X2, X3)
DELETEB_IN_AGA(s(X1), tree(s(X2), X3, void), tree(s(X2), X4, void)) → U48_AGA(X1, X2, X3, X4, lessA_in_ag(X1, X2))
DELETEB_IN_AGA(s(X1), tree(s(X2), X3, void), tree(s(X2), X4, void)) → LESSA_IN_AG(X1, X2)
DELETEB_IN_AGA(s(X1), tree(s(X2), X3, void), tree(s(X2), X4, void)) → U49_AGA(X1, X2, X3, X4, lesscA_in_ag(X1, X2))
U49_AGA(X1, X2, X3, X4, lesscA_out_ag(X1, X2)) → U50_AGA(X1, X2, X3, X4, deleteK_in_gga(s(X1), X3, X4))
U49_AGA(X1, X2, X3, X4, lesscA_out_ag(X1, X2)) → DELETEK_IN_GGA(s(X1), X3, X4)
DELETEB_IN_AGA(s(X1), tree(0, X2, void), tree(0, X2, X3)) → U51_AGA(X1, X2, X3, deleteB_in_aga(s(X1), void, X3))
DELETEB_IN_AGA(s(X1), tree(0, X2, void), tree(0, X2, X3)) → DELETEB_IN_AGA(s(X1), void, X3)
DELETEB_IN_AGA(s(X1), tree(s(X2), X3, void), tree(s(X2), X3, X4)) → U52_AGA(X1, X2, X3, X4, lessF_in_ga(X2, X1))
DELETEB_IN_AGA(s(X1), tree(s(X2), X3, void), tree(s(X2), X3, X4)) → LESSF_IN_GA(X2, X1)
DELETEB_IN_AGA(s(X1), tree(s(X2), X3, void), tree(s(X2), X3, X4)) → U53_AGA(X1, X2, X3, X4, lesscF_in_ga(X2, X1))
U53_AGA(X1, X2, X3, X4, lesscF_out_ga(X2, X1)) → U54_AGA(X1, X2, X3, X4, deleteB_in_aga(s(X1), void, X4))
U53_AGA(X1, X2, X3, X4, lesscF_out_ga(X2, X1)) → DELETEB_IN_AGA(s(X1), void, X4)
DELETEB_IN_AGA(X1, tree(X1, X2, tree(X3, X4, X5)), tree(X6, X2, tree(X3, X7, X8))) → U55_AGA(X1, X2, X3, X4, X5, X6, X7, X8, delminG_in_gaa(X4, X6, X7))
DELETEB_IN_AGA(X1, tree(X1, X2, tree(X3, X4, X5)), tree(X6, X2, tree(X3, X7, X8))) → DELMING_IN_GAA(X4, X6, X7)
DELETEB_IN_AGA(X1, tree(X2, X3, X4), tree(X2, X5, X4)) → U56_AGA(X1, X2, X3, X4, X5, lessA_in_ag(X1, X2))
DELETEB_IN_AGA(X1, tree(X2, X3, X4), tree(X2, X5, X4)) → LESSA_IN_AG(X1, X2)
DELETEB_IN_AGA(X1, tree(X2, X3, X4), tree(X2, X5, X4)) → U57_AGA(X1, X2, X3, X4, X5, lesscA_in_ag(X1, X2))
U57_AGA(X1, X2, X3, X4, X5, lesscA_out_ag(X1, X2)) → U58_AGA(X1, X2, X3, X4, X5, deleteK_in_gga(X1, X3, X5))
U57_AGA(X1, X2, X3, X4, X5, lesscA_out_ag(X1, X2)) → DELETEK_IN_GGA(X1, X3, X5)
DELETEB_IN_AGA(X1, tree(X2, X3, X4), tree(X2, X3, X5)) → U59_AGA(X1, X2, X3, X4, X5, pL_in_gaga(X2, X1, X4, X5))
DELETEB_IN_AGA(X1, tree(X2, X3, X4), tree(X2, X3, X5)) → PL_IN_GAGA(X2, X1, X4, X5)
PL_IN_GAGA(X1, X2, X3, X4) → U21_GAGA(X1, X2, X3, X4, lessF_in_ga(X1, X2))
PL_IN_GAGA(X1, X2, X3, X4) → LESSF_IN_GA(X1, X2)
PL_IN_GAGA(X1, X2, X3, X4) → U22_GAGA(X1, X2, X3, X4, lesscF_in_ga(X1, X2))
U22_GAGA(X1, X2, X3, X4, lesscF_out_ga(X1, X2)) → U23_GAGA(X1, X2, X3, X4, deleteB_in_aga(X2, X3, X4))
U22_GAGA(X1, X2, X3, X4, lesscF_out_ga(X1, X2)) → DELETEB_IN_AGA(X2, X3, X4)
DELETEB_IN_AGA(0, tree(s(X1), X2, X3), tree(s(X1), X4, X3)) → U60_AGA(X1, X2, X3, X4, deleteK_in_gga(0, X2, X4))
DELETEB_IN_AGA(0, tree(s(X1), X2, X3), tree(s(X1), X4, X3)) → DELETEK_IN_GGA(0, X2, X4)
DELETEB_IN_AGA(s(X1), tree(s(X2), X3, X4), tree(s(X2), X5, X4)) → U61_AGA(X1, X2, X3, X4, X5, lessA_in_ag(X1, X2))
DELETEB_IN_AGA(s(X1), tree(s(X2), X3, X4), tree(s(X2), X5, X4)) → LESSA_IN_AG(X1, X2)
DELETEB_IN_AGA(s(X1), tree(s(X2), X3, X4), tree(s(X2), X5, X4)) → U62_AGA(X1, X2, X3, X4, X5, lesscA_in_ag(X1, X2))
U62_AGA(X1, X2, X3, X4, X5, lesscA_out_ag(X1, X2)) → U63_AGA(X1, X2, X3, X4, X5, deleteK_in_gga(s(X1), X3, X5))
U62_AGA(X1, X2, X3, X4, X5, lesscA_out_ag(X1, X2)) → DELETEK_IN_GGA(s(X1), X3, X5)
DELETEB_IN_AGA(s(X1), tree(0, X2, X3), tree(0, X2, X4)) → U64_AGA(X1, X2, X3, X4, deleteB_in_aga(s(X1), X3, X4))
DELETEB_IN_AGA(s(X1), tree(0, X2, X3), tree(0, X2, X4)) → DELETEB_IN_AGA(s(X1), X3, X4)
DELETEB_IN_AGA(s(X1), tree(s(X2), X3, X4), tree(s(X2), X3, X5)) → U65_AGA(X1, X2, X3, X4, X5, lessF_in_ga(X2, X1))
DELETEB_IN_AGA(s(X1), tree(s(X2), X3, X4), tree(s(X2), X3, X5)) → LESSF_IN_GA(X2, X1)
DELETEB_IN_AGA(s(X1), tree(s(X2), X3, X4), tree(s(X2), X3, X5)) → U66_AGA(X1, X2, X3, X4, X5, lesscF_in_ga(X2, X1))
U66_AGA(X1, X2, X3, X4, X5, lesscF_out_ga(X2, X1)) → U67_AGA(X1, X2, X3, X4, X5, deleteB_in_aga(s(X1), X4, X5))
U66_AGA(X1, X2, X3, X4, X5, lesscF_out_ga(X2, X1)) → DELETEB_IN_AGA(s(X1), X4, X5)
The TRS R consists of the following rules:
lesscF_in_ga(0, s(X1)) → lesscF_out_ga(0, s(X1))
lesscF_in_ga(s(X1), s(X2)) → U104_ga(X1, X2, lesscF_in_ga(X1, X2))
U104_ga(X1, X2, lesscF_out_ga(X1, X2)) → lesscF_out_ga(s(X1), s(X2))
lesscA_in_gg(0, s(X1)) → lesscA_out_gg(0, s(X1))
lesscA_in_gg(s(X1), s(X2)) → U69_gg(X1, X2, lesscA_in_gg(X1, X2))
U69_gg(X1, X2, lesscA_out_gg(X1, X2)) → lesscA_out_gg(s(X1), s(X2))
lesscA_in_ag(0, s(X1)) → lesscA_out_ag(0, s(X1))
lesscA_in_ag(s(X1), s(X2)) → U69_ag(X1, X2, lesscA_in_ag(X1, X2))
U69_ag(X1, X2, lesscA_out_ag(X1, X2)) → lesscA_out_ag(s(X1), s(X2))
lesscM_in_gg(0, s(X1)) → lesscM_out_gg(0, s(X1))
lesscM_in_gg(s(X1), s(X2)) → U110_gg(X1, X2, lesscM_in_gg(X1, X2))
U110_gg(X1, X2, lesscM_out_gg(X1, X2)) → lesscM_out_gg(s(X1), s(X2))
The argument filtering Pi contains the following mapping:
deleteB_in_aga(
x1,
x2,
x3) =
deleteB_in_aga(
x2)
tree(
x1,
x2,
x3) =
tree(
x1,
x2,
x3)
void =
void
pC_in_aga(
x1,
x2,
x3) =
pC_in_aga(
x2)
lessA_in_ag(
x1,
x2) =
lessA_in_ag(
x2)
s(
x1) =
s(
x1)
pD_in_gaa(
x1,
x2,
x3) =
pD_in_gaa(
x1)
lessF_in_ga(
x1,
x2) =
lessF_in_ga(
x1)
lesscF_in_ga(
x1,
x2) =
lesscF_in_ga(
x1)
0 =
0
lesscF_out_ga(
x1,
x2) =
lesscF_out_ga(
x1)
U104_ga(
x1,
x2,
x3) =
U104_ga(
x1,
x3)
delminG_in_gaa(
x1,
x2,
x3) =
delminG_in_gaa(
x1)
pH_in_gaga(
x1,
x2,
x3,
x4) =
pH_in_gaga(
x1,
x3)
lesscA_in_gg(
x1,
x2) =
lesscA_in_gg(
x1,
x2)
lesscA_out_gg(
x1,
x2) =
lesscA_out_gg(
x1,
x2)
U69_gg(
x1,
x2,
x3) =
U69_gg(
x1,
x2,
x3)
lesscA_in_ag(
x1,
x2) =
lesscA_in_ag(
x2)
lesscA_out_ag(
x1,
x2) =
lesscA_out_ag(
x1,
x2)
U69_ag(
x1,
x2,
x3) =
U69_ag(
x2,
x3)
pI_in_ggga(
x1,
x2,
x3,
x4) =
pI_in_ggga(
x1,
x2,
x3)
lessM_in_gg(
x1,
x2) =
lessM_in_gg(
x1,
x2)
lesscM_in_gg(
x1,
x2) =
lesscM_in_gg(
x1,
x2)
lesscM_out_gg(
x1,
x2) =
lesscM_out_gg(
x1,
x2)
U110_gg(
x1,
x2,
x3) =
U110_gg(
x1,
x2,
x3)
deleteK_in_gga(
x1,
x2,
x3) =
deleteK_in_gga(
x1,
x2)
pJ_in_ggga(
x1,
x2,
x3,
x4) =
pJ_in_ggga(
x1,
x2,
x3)
pL_in_gaga(
x1,
x2,
x3,
x4) =
pL_in_gaga(
x1,
x3)
DELETEB_IN_AGA(
x1,
x2,
x3) =
DELETEB_IN_AGA(
x2)
U24_AGA(
x1,
x2,
x3,
x4) =
U24_AGA(
x2,
x4)
PC_IN_AGA(
x1,
x2,
x3) =
PC_IN_AGA(
x2)
U7_AGA(
x1,
x2,
x3,
x4) =
U7_AGA(
x2,
x4)
LESSA_IN_AG(
x1,
x2) =
LESSA_IN_AG(
x2)
U1_AG(
x1,
x2,
x3) =
U1_AG(
x2,
x3)
U25_AGA(
x1,
x2,
x3,
x4) =
U25_AGA(
x2,
x4)
PD_IN_GAA(
x1,
x2,
x3) =
PD_IN_GAA(
x1)
U3_GAA(
x1,
x2,
x3,
x4) =
U3_GAA(
x1,
x4)
LESSF_IN_GA(
x1,
x2) =
LESSF_IN_GA(
x1)
U2_GA(
x1,
x2,
x3) =
U2_GA(
x1,
x3)
U4_GAA(
x1,
x2,
x3,
x4) =
U4_GAA(
x1,
x4)
U5_GAA(
x1,
x2,
x3,
x4) =
U5_GAA(
x1,
x4)
U26_AGA(
x1,
x2,
x3,
x4) =
U26_AGA(
x2,
x4)
U27_AGA(
x1,
x2,
x3) =
U27_AGA(
x3)
U28_AGA(
x1,
x2,
x3,
x4) =
U28_AGA(
x2,
x4)
U29_AGA(
x1,
x2,
x3,
x4) =
U29_AGA(
x2,
x4)
U30_AGA(
x1,
x2,
x3,
x4) =
U30_AGA(
x2,
x4)
U31_AGA(
x1,
x2,
x3,
x4,
x5,
x6,
x7,
x8) =
U31_AGA(
x1,
x2,
x3,
x4,
x8)
DELMING_IN_GAA(
x1,
x2,
x3) =
DELMING_IN_GAA(
x1)
U6_GAA(
x1,
x2,
x3,
x4,
x5,
x6,
x7) =
U6_GAA(
x1,
x2,
x3,
x7)
U32_AGA(
x1,
x2,
x3,
x4,
x5) =
U32_AGA(
x2,
x3,
x5)
U33_AGA(
x1,
x2,
x3,
x4,
x5) =
U33_AGA(
x2,
x3,
x5)
PH_IN_GAGA(
x1,
x2,
x3,
x4) =
PH_IN_GAGA(
x1,
x3)
U8_GAGA(
x1,
x2,
x3,
x4,
x5) =
U8_GAGA(
x1,
x3,
x5)
U9_GAGA(
x1,
x2,
x3,
x4,
x5) =
U9_GAGA(
x1,
x3,
x5)
U10_GAGA(
x1,
x2,
x3,
x4,
x5) =
U10_GAGA(
x1,
x3,
x5)
U34_AGA(
x1,
x2,
x3,
x4,
x5) =
U34_AGA(
x2,
x3,
x5)
U35_AGA(
x1,
x2,
x3,
x4) =
U35_AGA(
x2,
x4)
U36_AGA(
x1,
x2,
x3,
x4,
x5) =
U36_AGA(
x2,
x3,
x5)
U37_AGA(
x1,
x2,
x3,
x4,
x5) =
U37_AGA(
x2,
x3,
x5)
U38_AGA(
x1,
x2,
x3,
x4,
x5) =
U38_AGA(
x2,
x3,
x5)
U39_AGA(
x1,
x2,
x3,
x4,
x5) =
U39_AGA(
x2,
x3,
x5)
U40_AGA(
x1,
x2,
x3,
x4,
x5,
x6,
x7) =
U40_AGA(
x1,
x2,
x3,
x4,
x7)
U41_AGA(
x1,
x2,
x3,
x4,
x5,
x6,
x7) =
U41_AGA(
x1,
x2,
x3,
x4,
x7)
U42_AGA(
x1,
x2,
x3,
x4,
x5,
x6,
x7) =
U42_AGA(
x2,
x3,
x4,
x5,
x7)
U43_AGA(
x1,
x2,
x3,
x4,
x5,
x6,
x7) =
U43_AGA(
x1,
x2,
x3,
x4,
x5,
x7)
PI_IN_GGGA(
x1,
x2,
x3,
x4) =
PI_IN_GGGA(
x1,
x2,
x3)
U12_GGGA(
x1,
x2,
x3,
x4,
x5) =
U12_GGGA(
x1,
x2,
x3,
x5)
LESSM_IN_GG(
x1,
x2) =
LESSM_IN_GG(
x1,
x2)
U11_GG(
x1,
x2,
x3) =
U11_GG(
x1,
x2,
x3)
U13_GGGA(
x1,
x2,
x3,
x4,
x5) =
U13_GGGA(
x1,
x2,
x3,
x5)
U14_GGGA(
x1,
x2,
x3,
x4,
x5) =
U14_GGGA(
x1,
x2,
x3,
x5)
DELETEK_IN_GGA(
x1,
x2,
x3) =
DELETEK_IN_GGA(
x1,
x2)
U15_GGA(
x1,
x2,
x3,
x4,
x5,
x6) =
U15_GGA(
x1,
x2,
x3,
x6)
U16_GGA(
x1,
x2,
x3,
x4,
x5,
x6) =
U16_GGA(
x1,
x2,
x3,
x4,
x6)
U17_GGA(
x1,
x2,
x3,
x4,
x5,
x6) =
U17_GGA(
x1,
x2,
x3,
x4,
x6)
PJ_IN_GGGA(
x1,
x2,
x3,
x4) =
PJ_IN_GGGA(
x1,
x2,
x3)
U18_GGGA(
x1,
x2,
x3,
x4,
x5) =
U18_GGGA(
x1,
x2,
x3,
x5)
U19_GGGA(
x1,
x2,
x3,
x4,
x5) =
U19_GGGA(
x1,
x2,
x3,
x5)
U20_GGGA(
x1,
x2,
x3,
x4,
x5) =
U20_GGGA(
x1,
x2,
x3,
x5)
U44_AGA(
x1,
x2,
x3,
x4,
x5,
x6,
x7) =
U44_AGA(
x2,
x3,
x4,
x5,
x7)
U45_AGA(
x1,
x2,
x3,
x4,
x5,
x6,
x7) =
U45_AGA(
x1,
x2,
x3,
x4,
x5,
x7)
U46_AGA(
x1,
x2,
x3,
x4,
x5) =
U46_AGA(
x2,
x3,
x5)
U47_AGA(
x1,
x2,
x3,
x4) =
U47_AGA(
x1,
x2,
x4)
U48_AGA(
x1,
x2,
x3,
x4,
x5) =
U48_AGA(
x2,
x3,
x5)
U49_AGA(
x1,
x2,
x3,
x4,
x5) =
U49_AGA(
x2,
x3,
x5)
U50_AGA(
x1,
x2,
x3,
x4,
x5) =
U50_AGA(
x1,
x2,
x3,
x5)
U51_AGA(
x1,
x2,
x3,
x4) =
U51_AGA(
x2,
x4)
U52_AGA(
x1,
x2,
x3,
x4,
x5) =
U52_AGA(
x2,
x3,
x5)
U53_AGA(
x1,
x2,
x3,
x4,
x5) =
U53_AGA(
x2,
x3,
x5)
U54_AGA(
x1,
x2,
x3,
x4,
x5) =
U54_AGA(
x2,
x3,
x5)
U55_AGA(
x1,
x2,
x3,
x4,
x5,
x6,
x7,
x8,
x9) =
U55_AGA(
x1,
x2,
x3,
x4,
x5,
x9)
U56_AGA(
x1,
x2,
x3,
x4,
x5,
x6) =
U56_AGA(
x2,
x3,
x4,
x6)
U57_AGA(
x1,
x2,
x3,
x4,
x5,
x6) =
U57_AGA(
x2,
x3,
x4,
x6)
U58_AGA(
x1,
x2,
x3,
x4,
x5,
x6) =
U58_AGA(
x1,
x2,
x3,
x4,
x6)
U59_AGA(
x1,
x2,
x3,
x4,
x5,
x6) =
U59_AGA(
x2,
x3,
x4,
x6)
PL_IN_GAGA(
x1,
x2,
x3,
x4) =
PL_IN_GAGA(
x1,
x3)
U21_GAGA(
x1,
x2,
x3,
x4,
x5) =
U21_GAGA(
x1,
x3,
x5)
U22_GAGA(
x1,
x2,
x3,
x4,
x5) =
U22_GAGA(
x1,
x3,
x5)
U23_GAGA(
x1,
x2,
x3,
x4,
x5) =
U23_GAGA(
x1,
x3,
x5)
U60_AGA(
x1,
x2,
x3,
x4,
x5) =
U60_AGA(
x1,
x2,
x3,
x5)
U61_AGA(
x1,
x2,
x3,
x4,
x5,
x6) =
U61_AGA(
x2,
x3,
x4,
x6)
U62_AGA(
x1,
x2,
x3,
x4,
x5,
x6) =
U62_AGA(
x2,
x3,
x4,
x6)
U63_AGA(
x1,
x2,
x3,
x4,
x5,
x6) =
U63_AGA(
x1,
x2,
x3,
x4,
x6)
U64_AGA(
x1,
x2,
x3,
x4,
x5) =
U64_AGA(
x2,
x3,
x5)
U65_AGA(
x1,
x2,
x3,
x4,
x5,
x6) =
U65_AGA(
x2,
x3,
x4,
x6)
U66_AGA(
x1,
x2,
x3,
x4,
x5,
x6) =
U66_AGA(
x2,
x3,
x4,
x6)
U67_AGA(
x1,
x2,
x3,
x4,
x5,
x6) =
U67_AGA(
x2,
x3,
x4,
x6)
We have to consider all (P,R,Pi)-chains
Infinitary Constructor Rewriting Termination of PiDP implies Termination of TRIPLES
(6) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
DELETEB_IN_AGA(X1, tree(X2, void, void), tree(X2, X3, void)) → U24_AGA(X1, X2, X3, pC_in_aga(X1, X2, X3))
DELETEB_IN_AGA(X1, tree(X2, void, void), tree(X2, X3, void)) → PC_IN_AGA(X1, X2, X3)
PC_IN_AGA(X1, X2, X3) → U7_AGA(X1, X2, X3, lessA_in_ag(X1, X2))
PC_IN_AGA(X1, X2, X3) → LESSA_IN_AG(X1, X2)
LESSA_IN_AG(s(X1), s(X2)) → U1_AG(X1, X2, lessA_in_ag(X1, X2))
LESSA_IN_AG(s(X1), s(X2)) → LESSA_IN_AG(X1, X2)
DELETEB_IN_AGA(X1, tree(X2, void, void), tree(X2, void, X3)) → U25_AGA(X1, X2, X3, pD_in_gaa(X2, X1, X3))
DELETEB_IN_AGA(X1, tree(X2, void, void), tree(X2, void, X3)) → PD_IN_GAA(X2, X1, X3)
PD_IN_GAA(X1, X2, X3) → U3_GAA(X1, X2, X3, lessF_in_ga(X1, X2))
PD_IN_GAA(X1, X2, X3) → LESSF_IN_GA(X1, X2)
LESSF_IN_GA(s(X1), s(X2)) → U2_GA(X1, X2, lessF_in_ga(X1, X2))
LESSF_IN_GA(s(X1), s(X2)) → LESSF_IN_GA(X1, X2)
PD_IN_GAA(X1, X2, X3) → U4_GAA(X1, X2, X3, lesscF_in_ga(X1, X2))
U4_GAA(X1, X2, X3, lesscF_out_ga(X1, X2)) → U5_GAA(X1, X2, X3, deleteB_in_aga(X2, void, X3))
U4_GAA(X1, X2, X3, lesscF_out_ga(X1, X2)) → DELETEB_IN_AGA(X2, void, X3)
DELETEB_IN_AGA(s(X1), tree(s(X2), void, void), tree(s(X2), X3, void)) → U26_AGA(X1, X2, X3, lessA_in_ag(X1, X2))
DELETEB_IN_AGA(s(X1), tree(s(X2), void, void), tree(s(X2), X3, void)) → LESSA_IN_AG(X1, X2)
DELETEB_IN_AGA(s(X1), tree(0, void, void), tree(0, void, X2)) → U27_AGA(X1, X2, deleteB_in_aga(s(X1), void, X2))
DELETEB_IN_AGA(s(X1), tree(0, void, void), tree(0, void, X2)) → DELETEB_IN_AGA(s(X1), void, X2)
DELETEB_IN_AGA(s(X1), tree(s(X2), void, void), tree(s(X2), void, X3)) → U28_AGA(X1, X2, X3, lessF_in_ga(X2, X1))
DELETEB_IN_AGA(s(X1), tree(s(X2), void, void), tree(s(X2), void, X3)) → LESSF_IN_GA(X2, X1)
DELETEB_IN_AGA(s(X1), tree(s(X2), void, void), tree(s(X2), void, X3)) → U29_AGA(X1, X2, X3, lesscF_in_ga(X2, X1))
U29_AGA(X1, X2, X3, lesscF_out_ga(X2, X1)) → U30_AGA(X1, X2, X3, deleteB_in_aga(s(X1), void, X3))
U29_AGA(X1, X2, X3, lesscF_out_ga(X2, X1)) → DELETEB_IN_AGA(s(X1), void, X3)
DELETEB_IN_AGA(X1, tree(X1, void, tree(X2, X3, X4)), tree(X5, void, tree(X2, X6, X7))) → U31_AGA(X1, X2, X3, X4, X5, X6, X7, delminG_in_gaa(X3, X5, X6))
DELETEB_IN_AGA(X1, tree(X1, void, tree(X2, X3, X4)), tree(X5, void, tree(X2, X6, X7))) → DELMING_IN_GAA(X3, X5, X6)
DELMING_IN_GAA(tree(X1, X2, X3), X4, tree(X1, X5, X6)) → U6_GAA(X1, X2, X3, X4, X5, X6, delminG_in_gaa(X2, X4, X5))
DELMING_IN_GAA(tree(X1, X2, X3), X4, tree(X1, X5, X6)) → DELMING_IN_GAA(X2, X4, X5)
DELETEB_IN_AGA(X1, tree(X2, void, X3), tree(X2, X4, X3)) → U32_AGA(X1, X2, X3, X4, pC_in_aga(X1, X2, X4))
DELETEB_IN_AGA(X1, tree(X2, void, X3), tree(X2, X4, X3)) → PC_IN_AGA(X1, X2, X4)
DELETEB_IN_AGA(X1, tree(X2, void, X3), tree(X2, void, X4)) → U33_AGA(X1, X2, X3, X4, pH_in_gaga(X2, X1, X3, X4))
DELETEB_IN_AGA(X1, tree(X2, void, X3), tree(X2, void, X4)) → PH_IN_GAGA(X2, X1, X3, X4)
PH_IN_GAGA(X1, X2, X3, X4) → U8_GAGA(X1, X2, X3, X4, lessF_in_ga(X1, X2))
PH_IN_GAGA(X1, X2, X3, X4) → LESSF_IN_GA(X1, X2)
PH_IN_GAGA(X1, X2, X3, X4) → U9_GAGA(X1, X2, X3, X4, lesscF_in_ga(X1, X2))
U9_GAGA(X1, X2, X3, X4, lesscF_out_ga(X1, X2)) → U10_GAGA(X1, X2, X3, X4, deleteB_in_aga(X2, X3, X4))
U9_GAGA(X1, X2, X3, X4, lesscF_out_ga(X1, X2)) → DELETEB_IN_AGA(X2, X3, X4)
DELETEB_IN_AGA(s(X1), tree(s(X2), void, X3), tree(s(X2), X4, X3)) → U34_AGA(X1, X2, X3, X4, lessA_in_ag(X1, X2))
DELETEB_IN_AGA(s(X1), tree(s(X2), void, X3), tree(s(X2), X4, X3)) → LESSA_IN_AG(X1, X2)
DELETEB_IN_AGA(s(X1), tree(0, void, X2), tree(0, void, X3)) → U35_AGA(X1, X2, X3, deleteB_in_aga(s(X1), X2, X3))
DELETEB_IN_AGA(s(X1), tree(0, void, X2), tree(0, void, X3)) → DELETEB_IN_AGA(s(X1), X2, X3)
DELETEB_IN_AGA(s(X1), tree(s(X2), void, X3), tree(s(X2), void, X4)) → U36_AGA(X1, X2, X3, X4, lessF_in_ga(X2, X1))
DELETEB_IN_AGA(s(X1), tree(s(X2), void, X3), tree(s(X2), void, X4)) → LESSF_IN_GA(X2, X1)
DELETEB_IN_AGA(s(X1), tree(s(X2), void, X3), tree(s(X2), void, X4)) → U37_AGA(X1, X2, X3, X4, lesscF_in_ga(X2, X1))
U37_AGA(X1, X2, X3, X4, lesscF_out_ga(X2, X1)) → U38_AGA(X1, X2, X3, X4, deleteB_in_aga(s(X1), X3, X4))
U37_AGA(X1, X2, X3, X4, lesscF_out_ga(X2, X1)) → DELETEB_IN_AGA(s(X1), X3, X4)
DELETEB_IN_AGA(X1, tree(X2, X3, void), tree(X2, X4, void)) → U39_AGA(X1, X2, X3, X4, lessA_in_ag(X1, X2))
DELETEB_IN_AGA(X1, tree(X2, X3, void), tree(X2, X4, void)) → LESSA_IN_AG(X1, X2)
DELETEB_IN_AGA(X1, tree(X2, tree(X1, X3, X4), void), tree(X2, tree(X5, X3, X6), void)) → U40_AGA(X1, X2, X3, X4, X5, X6, lesscA_in_gg(X1, X2))
U40_AGA(X1, X2, X3, X4, X5, X6, lesscA_out_gg(X1, X2)) → U41_AGA(X1, X2, X3, X4, X5, X6, delminG_in_gaa(X4, X5, X6))
U40_AGA(X1, X2, X3, X4, X5, X6, lesscA_out_gg(X1, X2)) → DELMING_IN_GAA(X4, X5, X6)
DELETEB_IN_AGA(X1, tree(X2, tree(X3, X4, X5), void), tree(X2, tree(X3, X6, X5), void)) → U42_AGA(X1, X2, X3, X4, X5, X6, lesscA_in_ag(X1, X2))
U42_AGA(X1, X2, X3, X4, X5, X6, lesscA_out_ag(X1, X2)) → U43_AGA(X1, X2, X3, X4, X5, X6, pI_in_ggga(X1, X3, X4, X6))
U42_AGA(X1, X2, X3, X4, X5, X6, lesscA_out_ag(X1, X2)) → PI_IN_GGGA(X1, X3, X4, X6)
PI_IN_GGGA(X1, X2, X3, X4) → U12_GGGA(X1, X2, X3, X4, lessM_in_gg(X1, X2))
PI_IN_GGGA(X1, X2, X3, X4) → LESSM_IN_GG(X1, X2)
LESSM_IN_GG(s(X1), s(X2)) → U11_GG(X1, X2, lessM_in_gg(X1, X2))
LESSM_IN_GG(s(X1), s(X2)) → LESSM_IN_GG(X1, X2)
PI_IN_GGGA(X1, X2, X3, X4) → U13_GGGA(X1, X2, X3, X4, lesscM_in_gg(X1, X2))
U13_GGGA(X1, X2, X3, X4, lesscM_out_gg(X1, X2)) → U14_GGGA(X1, X2, X3, X4, deleteK_in_gga(X1, X3, X4))
U13_GGGA(X1, X2, X3, X4, lesscM_out_gg(X1, X2)) → DELETEK_IN_GGA(X1, X3, X4)
DELETEK_IN_GGA(X1, tree(X1, X2, X3), tree(X4, X2, X5)) → U15_GGA(X1, X2, X3, X4, X5, delminG_in_gaa(X3, X4, X5))
DELETEK_IN_GGA(X1, tree(X1, X2, X3), tree(X4, X2, X5)) → DELMING_IN_GAA(X3, X4, X5)
DELETEK_IN_GGA(X1, tree(X2, X3, X4), tree(X2, X5, X4)) → U16_GGA(X1, X2, X3, X4, X5, pI_in_ggga(X1, X2, X3, X5))
DELETEK_IN_GGA(X1, tree(X2, X3, X4), tree(X2, X5, X4)) → PI_IN_GGGA(X1, X2, X3, X5)
DELETEK_IN_GGA(X1, tree(X2, X3, X4), tree(X2, X3, X5)) → U17_GGA(X1, X2, X3, X4, X5, pJ_in_ggga(X2, X1, X4, X5))
DELETEK_IN_GGA(X1, tree(X2, X3, X4), tree(X2, X3, X5)) → PJ_IN_GGGA(X2, X1, X4, X5)
PJ_IN_GGGA(X1, X2, X3, X4) → U18_GGGA(X1, X2, X3, X4, lessM_in_gg(X1, X2))
PJ_IN_GGGA(X1, X2, X3, X4) → LESSM_IN_GG(X1, X2)
PJ_IN_GGGA(X1, X2, X3, X4) → U19_GGGA(X1, X2, X3, X4, lesscM_in_gg(X1, X2))
U19_GGGA(X1, X2, X3, X4, lesscM_out_gg(X1, X2)) → U20_GGGA(X1, X2, X3, X4, deleteK_in_gga(X2, X3, X4))
U19_GGGA(X1, X2, X3, X4, lesscM_out_gg(X1, X2)) → DELETEK_IN_GGA(X2, X3, X4)
DELETEB_IN_AGA(X1, tree(X2, tree(X3, X4, X5), void), tree(X2, tree(X3, X4, X6), void)) → U44_AGA(X1, X2, X3, X4, X5, X6, lesscA_in_ag(X1, X2))
U44_AGA(X1, X2, X3, X4, X5, X6, lesscA_out_ag(X1, X2)) → U45_AGA(X1, X2, X3, X4, X5, X6, pJ_in_ggga(X3, X1, X5, X6))
U44_AGA(X1, X2, X3, X4, X5, X6, lesscA_out_ag(X1, X2)) → PJ_IN_GGGA(X3, X1, X5, X6)
DELETEB_IN_AGA(X1, tree(X2, X3, void), tree(X2, X3, X4)) → U46_AGA(X1, X2, X3, X4, pD_in_gaa(X2, X1, X4))
DELETEB_IN_AGA(X1, tree(X2, X3, void), tree(X2, X3, X4)) → PD_IN_GAA(X2, X1, X4)
DELETEB_IN_AGA(0, tree(s(X1), X2, void), tree(s(X1), X3, void)) → U47_AGA(X1, X2, X3, deleteK_in_gga(0, X2, X3))
DELETEB_IN_AGA(0, tree(s(X1), X2, void), tree(s(X1), X3, void)) → DELETEK_IN_GGA(0, X2, X3)
DELETEB_IN_AGA(s(X1), tree(s(X2), X3, void), tree(s(X2), X4, void)) → U48_AGA(X1, X2, X3, X4, lessA_in_ag(X1, X2))
DELETEB_IN_AGA(s(X1), tree(s(X2), X3, void), tree(s(X2), X4, void)) → LESSA_IN_AG(X1, X2)
DELETEB_IN_AGA(s(X1), tree(s(X2), X3, void), tree(s(X2), X4, void)) → U49_AGA(X1, X2, X3, X4, lesscA_in_ag(X1, X2))
U49_AGA(X1, X2, X3, X4, lesscA_out_ag(X1, X2)) → U50_AGA(X1, X2, X3, X4, deleteK_in_gga(s(X1), X3, X4))
U49_AGA(X1, X2, X3, X4, lesscA_out_ag(X1, X2)) → DELETEK_IN_GGA(s(X1), X3, X4)
DELETEB_IN_AGA(s(X1), tree(0, X2, void), tree(0, X2, X3)) → U51_AGA(X1, X2, X3, deleteB_in_aga(s(X1), void, X3))
DELETEB_IN_AGA(s(X1), tree(0, X2, void), tree(0, X2, X3)) → DELETEB_IN_AGA(s(X1), void, X3)
DELETEB_IN_AGA(s(X1), tree(s(X2), X3, void), tree(s(X2), X3, X4)) → U52_AGA(X1, X2, X3, X4, lessF_in_ga(X2, X1))
DELETEB_IN_AGA(s(X1), tree(s(X2), X3, void), tree(s(X2), X3, X4)) → LESSF_IN_GA(X2, X1)
DELETEB_IN_AGA(s(X1), tree(s(X2), X3, void), tree(s(X2), X3, X4)) → U53_AGA(X1, X2, X3, X4, lesscF_in_ga(X2, X1))
U53_AGA(X1, X2, X3, X4, lesscF_out_ga(X2, X1)) → U54_AGA(X1, X2, X3, X4, deleteB_in_aga(s(X1), void, X4))
U53_AGA(X1, X2, X3, X4, lesscF_out_ga(X2, X1)) → DELETEB_IN_AGA(s(X1), void, X4)
DELETEB_IN_AGA(X1, tree(X1, X2, tree(X3, X4, X5)), tree(X6, X2, tree(X3, X7, X8))) → U55_AGA(X1, X2, X3, X4, X5, X6, X7, X8, delminG_in_gaa(X4, X6, X7))
DELETEB_IN_AGA(X1, tree(X1, X2, tree(X3, X4, X5)), tree(X6, X2, tree(X3, X7, X8))) → DELMING_IN_GAA(X4, X6, X7)
DELETEB_IN_AGA(X1, tree(X2, X3, X4), tree(X2, X5, X4)) → U56_AGA(X1, X2, X3, X4, X5, lessA_in_ag(X1, X2))
DELETEB_IN_AGA(X1, tree(X2, X3, X4), tree(X2, X5, X4)) → LESSA_IN_AG(X1, X2)
DELETEB_IN_AGA(X1, tree(X2, X3, X4), tree(X2, X5, X4)) → U57_AGA(X1, X2, X3, X4, X5, lesscA_in_ag(X1, X2))
U57_AGA(X1, X2, X3, X4, X5, lesscA_out_ag(X1, X2)) → U58_AGA(X1, X2, X3, X4, X5, deleteK_in_gga(X1, X3, X5))
U57_AGA(X1, X2, X3, X4, X5, lesscA_out_ag(X1, X2)) → DELETEK_IN_GGA(X1, X3, X5)
DELETEB_IN_AGA(X1, tree(X2, X3, X4), tree(X2, X3, X5)) → U59_AGA(X1, X2, X3, X4, X5, pL_in_gaga(X2, X1, X4, X5))
DELETEB_IN_AGA(X1, tree(X2, X3, X4), tree(X2, X3, X5)) → PL_IN_GAGA(X2, X1, X4, X5)
PL_IN_GAGA(X1, X2, X3, X4) → U21_GAGA(X1, X2, X3, X4, lessF_in_ga(X1, X2))
PL_IN_GAGA(X1, X2, X3, X4) → LESSF_IN_GA(X1, X2)
PL_IN_GAGA(X1, X2, X3, X4) → U22_GAGA(X1, X2, X3, X4, lesscF_in_ga(X1, X2))
U22_GAGA(X1, X2, X3, X4, lesscF_out_ga(X1, X2)) → U23_GAGA(X1, X2, X3, X4, deleteB_in_aga(X2, X3, X4))
U22_GAGA(X1, X2, X3, X4, lesscF_out_ga(X1, X2)) → DELETEB_IN_AGA(X2, X3, X4)
DELETEB_IN_AGA(0, tree(s(X1), X2, X3), tree(s(X1), X4, X3)) → U60_AGA(X1, X2, X3, X4, deleteK_in_gga(0, X2, X4))
DELETEB_IN_AGA(0, tree(s(X1), X2, X3), tree(s(X1), X4, X3)) → DELETEK_IN_GGA(0, X2, X4)
DELETEB_IN_AGA(s(X1), tree(s(X2), X3, X4), tree(s(X2), X5, X4)) → U61_AGA(X1, X2, X3, X4, X5, lessA_in_ag(X1, X2))
DELETEB_IN_AGA(s(X1), tree(s(X2), X3, X4), tree(s(X2), X5, X4)) → LESSA_IN_AG(X1, X2)
DELETEB_IN_AGA(s(X1), tree(s(X2), X3, X4), tree(s(X2), X5, X4)) → U62_AGA(X1, X2, X3, X4, X5, lesscA_in_ag(X1, X2))
U62_AGA(X1, X2, X3, X4, X5, lesscA_out_ag(X1, X2)) → U63_AGA(X1, X2, X3, X4, X5, deleteK_in_gga(s(X1), X3, X5))
U62_AGA(X1, X2, X3, X4, X5, lesscA_out_ag(X1, X2)) → DELETEK_IN_GGA(s(X1), X3, X5)
DELETEB_IN_AGA(s(X1), tree(0, X2, X3), tree(0, X2, X4)) → U64_AGA(X1, X2, X3, X4, deleteB_in_aga(s(X1), X3, X4))
DELETEB_IN_AGA(s(X1), tree(0, X2, X3), tree(0, X2, X4)) → DELETEB_IN_AGA(s(X1), X3, X4)
DELETEB_IN_AGA(s(X1), tree(s(X2), X3, X4), tree(s(X2), X3, X5)) → U65_AGA(X1, X2, X3, X4, X5, lessF_in_ga(X2, X1))
DELETEB_IN_AGA(s(X1), tree(s(X2), X3, X4), tree(s(X2), X3, X5)) → LESSF_IN_GA(X2, X1)
DELETEB_IN_AGA(s(X1), tree(s(X2), X3, X4), tree(s(X2), X3, X5)) → U66_AGA(X1, X2, X3, X4, X5, lesscF_in_ga(X2, X1))
U66_AGA(X1, X2, X3, X4, X5, lesscF_out_ga(X2, X1)) → U67_AGA(X1, X2, X3, X4, X5, deleteB_in_aga(s(X1), X4, X5))
U66_AGA(X1, X2, X3, X4, X5, lesscF_out_ga(X2, X1)) → DELETEB_IN_AGA(s(X1), X4, X5)
The TRS R consists of the following rules:
lesscF_in_ga(0, s(X1)) → lesscF_out_ga(0, s(X1))
lesscF_in_ga(s(X1), s(X2)) → U104_ga(X1, X2, lesscF_in_ga(X1, X2))
U104_ga(X1, X2, lesscF_out_ga(X1, X2)) → lesscF_out_ga(s(X1), s(X2))
lesscA_in_gg(0, s(X1)) → lesscA_out_gg(0, s(X1))
lesscA_in_gg(s(X1), s(X2)) → U69_gg(X1, X2, lesscA_in_gg(X1, X2))
U69_gg(X1, X2, lesscA_out_gg(X1, X2)) → lesscA_out_gg(s(X1), s(X2))
lesscA_in_ag(0, s(X1)) → lesscA_out_ag(0, s(X1))
lesscA_in_ag(s(X1), s(X2)) → U69_ag(X1, X2, lesscA_in_ag(X1, X2))
U69_ag(X1, X2, lesscA_out_ag(X1, X2)) → lesscA_out_ag(s(X1), s(X2))
lesscM_in_gg(0, s(X1)) → lesscM_out_gg(0, s(X1))
lesscM_in_gg(s(X1), s(X2)) → U110_gg(X1, X2, lesscM_in_gg(X1, X2))
U110_gg(X1, X2, lesscM_out_gg(X1, X2)) → lesscM_out_gg(s(X1), s(X2))
The argument filtering Pi contains the following mapping:
deleteB_in_aga(
x1,
x2,
x3) =
deleteB_in_aga(
x2)
tree(
x1,
x2,
x3) =
tree(
x1,
x2,
x3)
void =
void
pC_in_aga(
x1,
x2,
x3) =
pC_in_aga(
x2)
lessA_in_ag(
x1,
x2) =
lessA_in_ag(
x2)
s(
x1) =
s(
x1)
pD_in_gaa(
x1,
x2,
x3) =
pD_in_gaa(
x1)
lessF_in_ga(
x1,
x2) =
lessF_in_ga(
x1)
lesscF_in_ga(
x1,
x2) =
lesscF_in_ga(
x1)
0 =
0
lesscF_out_ga(
x1,
x2) =
lesscF_out_ga(
x1)
U104_ga(
x1,
x2,
x3) =
U104_ga(
x1,
x3)
delminG_in_gaa(
x1,
x2,
x3) =
delminG_in_gaa(
x1)
pH_in_gaga(
x1,
x2,
x3,
x4) =
pH_in_gaga(
x1,
x3)
lesscA_in_gg(
x1,
x2) =
lesscA_in_gg(
x1,
x2)
lesscA_out_gg(
x1,
x2) =
lesscA_out_gg(
x1,
x2)
U69_gg(
x1,
x2,
x3) =
U69_gg(
x1,
x2,
x3)
lesscA_in_ag(
x1,
x2) =
lesscA_in_ag(
x2)
lesscA_out_ag(
x1,
x2) =
lesscA_out_ag(
x1,
x2)
U69_ag(
x1,
x2,
x3) =
U69_ag(
x2,
x3)
pI_in_ggga(
x1,
x2,
x3,
x4) =
pI_in_ggga(
x1,
x2,
x3)
lessM_in_gg(
x1,
x2) =
lessM_in_gg(
x1,
x2)
lesscM_in_gg(
x1,
x2) =
lesscM_in_gg(
x1,
x2)
lesscM_out_gg(
x1,
x2) =
lesscM_out_gg(
x1,
x2)
U110_gg(
x1,
x2,
x3) =
U110_gg(
x1,
x2,
x3)
deleteK_in_gga(
x1,
x2,
x3) =
deleteK_in_gga(
x1,
x2)
pJ_in_ggga(
x1,
x2,
x3,
x4) =
pJ_in_ggga(
x1,
x2,
x3)
pL_in_gaga(
x1,
x2,
x3,
x4) =
pL_in_gaga(
x1,
x3)
DELETEB_IN_AGA(
x1,
x2,
x3) =
DELETEB_IN_AGA(
x2)
U24_AGA(
x1,
x2,
x3,
x4) =
U24_AGA(
x2,
x4)
PC_IN_AGA(
x1,
x2,
x3) =
PC_IN_AGA(
x2)
U7_AGA(
x1,
x2,
x3,
x4) =
U7_AGA(
x2,
x4)
LESSA_IN_AG(
x1,
x2) =
LESSA_IN_AG(
x2)
U1_AG(
x1,
x2,
x3) =
U1_AG(
x2,
x3)
U25_AGA(
x1,
x2,
x3,
x4) =
U25_AGA(
x2,
x4)
PD_IN_GAA(
x1,
x2,
x3) =
PD_IN_GAA(
x1)
U3_GAA(
x1,
x2,
x3,
x4) =
U3_GAA(
x1,
x4)
LESSF_IN_GA(
x1,
x2) =
LESSF_IN_GA(
x1)
U2_GA(
x1,
x2,
x3) =
U2_GA(
x1,
x3)
U4_GAA(
x1,
x2,
x3,
x4) =
U4_GAA(
x1,
x4)
U5_GAA(
x1,
x2,
x3,
x4) =
U5_GAA(
x1,
x4)
U26_AGA(
x1,
x2,
x3,
x4) =
U26_AGA(
x2,
x4)
U27_AGA(
x1,
x2,
x3) =
U27_AGA(
x3)
U28_AGA(
x1,
x2,
x3,
x4) =
U28_AGA(
x2,
x4)
U29_AGA(
x1,
x2,
x3,
x4) =
U29_AGA(
x2,
x4)
U30_AGA(
x1,
x2,
x3,
x4) =
U30_AGA(
x2,
x4)
U31_AGA(
x1,
x2,
x3,
x4,
x5,
x6,
x7,
x8) =
U31_AGA(
x1,
x2,
x3,
x4,
x8)
DELMING_IN_GAA(
x1,
x2,
x3) =
DELMING_IN_GAA(
x1)
U6_GAA(
x1,
x2,
x3,
x4,
x5,
x6,
x7) =
U6_GAA(
x1,
x2,
x3,
x7)
U32_AGA(
x1,
x2,
x3,
x4,
x5) =
U32_AGA(
x2,
x3,
x5)
U33_AGA(
x1,
x2,
x3,
x4,
x5) =
U33_AGA(
x2,
x3,
x5)
PH_IN_GAGA(
x1,
x2,
x3,
x4) =
PH_IN_GAGA(
x1,
x3)
U8_GAGA(
x1,
x2,
x3,
x4,
x5) =
U8_GAGA(
x1,
x3,
x5)
U9_GAGA(
x1,
x2,
x3,
x4,
x5) =
U9_GAGA(
x1,
x3,
x5)
U10_GAGA(
x1,
x2,
x3,
x4,
x5) =
U10_GAGA(
x1,
x3,
x5)
U34_AGA(
x1,
x2,
x3,
x4,
x5) =
U34_AGA(
x2,
x3,
x5)
U35_AGA(
x1,
x2,
x3,
x4) =
U35_AGA(
x2,
x4)
U36_AGA(
x1,
x2,
x3,
x4,
x5) =
U36_AGA(
x2,
x3,
x5)
U37_AGA(
x1,
x2,
x3,
x4,
x5) =
U37_AGA(
x2,
x3,
x5)
U38_AGA(
x1,
x2,
x3,
x4,
x5) =
U38_AGA(
x2,
x3,
x5)
U39_AGA(
x1,
x2,
x3,
x4,
x5) =
U39_AGA(
x2,
x3,
x5)
U40_AGA(
x1,
x2,
x3,
x4,
x5,
x6,
x7) =
U40_AGA(
x1,
x2,
x3,
x4,
x7)
U41_AGA(
x1,
x2,
x3,
x4,
x5,
x6,
x7) =
U41_AGA(
x1,
x2,
x3,
x4,
x7)
U42_AGA(
x1,
x2,
x3,
x4,
x5,
x6,
x7) =
U42_AGA(
x2,
x3,
x4,
x5,
x7)
U43_AGA(
x1,
x2,
x3,
x4,
x5,
x6,
x7) =
U43_AGA(
x1,
x2,
x3,
x4,
x5,
x7)
PI_IN_GGGA(
x1,
x2,
x3,
x4) =
PI_IN_GGGA(
x1,
x2,
x3)
U12_GGGA(
x1,
x2,
x3,
x4,
x5) =
U12_GGGA(
x1,
x2,
x3,
x5)
LESSM_IN_GG(
x1,
x2) =
LESSM_IN_GG(
x1,
x2)
U11_GG(
x1,
x2,
x3) =
U11_GG(
x1,
x2,
x3)
U13_GGGA(
x1,
x2,
x3,
x4,
x5) =
U13_GGGA(
x1,
x2,
x3,
x5)
U14_GGGA(
x1,
x2,
x3,
x4,
x5) =
U14_GGGA(
x1,
x2,
x3,
x5)
DELETEK_IN_GGA(
x1,
x2,
x3) =
DELETEK_IN_GGA(
x1,
x2)
U15_GGA(
x1,
x2,
x3,
x4,
x5,
x6) =
U15_GGA(
x1,
x2,
x3,
x6)
U16_GGA(
x1,
x2,
x3,
x4,
x5,
x6) =
U16_GGA(
x1,
x2,
x3,
x4,
x6)
U17_GGA(
x1,
x2,
x3,
x4,
x5,
x6) =
U17_GGA(
x1,
x2,
x3,
x4,
x6)
PJ_IN_GGGA(
x1,
x2,
x3,
x4) =
PJ_IN_GGGA(
x1,
x2,
x3)
U18_GGGA(
x1,
x2,
x3,
x4,
x5) =
U18_GGGA(
x1,
x2,
x3,
x5)
U19_GGGA(
x1,
x2,
x3,
x4,
x5) =
U19_GGGA(
x1,
x2,
x3,
x5)
U20_GGGA(
x1,
x2,
x3,
x4,
x5) =
U20_GGGA(
x1,
x2,
x3,
x5)
U44_AGA(
x1,
x2,
x3,
x4,
x5,
x6,
x7) =
U44_AGA(
x2,
x3,
x4,
x5,
x7)
U45_AGA(
x1,
x2,
x3,
x4,
x5,
x6,
x7) =
U45_AGA(
x1,
x2,
x3,
x4,
x5,
x7)
U46_AGA(
x1,
x2,
x3,
x4,
x5) =
U46_AGA(
x2,
x3,
x5)
U47_AGA(
x1,
x2,
x3,
x4) =
U47_AGA(
x1,
x2,
x4)
U48_AGA(
x1,
x2,
x3,
x4,
x5) =
U48_AGA(
x2,
x3,
x5)
U49_AGA(
x1,
x2,
x3,
x4,
x5) =
U49_AGA(
x2,
x3,
x5)
U50_AGA(
x1,
x2,
x3,
x4,
x5) =
U50_AGA(
x1,
x2,
x3,
x5)
U51_AGA(
x1,
x2,
x3,
x4) =
U51_AGA(
x2,
x4)
U52_AGA(
x1,
x2,
x3,
x4,
x5) =
U52_AGA(
x2,
x3,
x5)
U53_AGA(
x1,
x2,
x3,
x4,
x5) =
U53_AGA(
x2,
x3,
x5)
U54_AGA(
x1,
x2,
x3,
x4,
x5) =
U54_AGA(
x2,
x3,
x5)
U55_AGA(
x1,
x2,
x3,
x4,
x5,
x6,
x7,
x8,
x9) =
U55_AGA(
x1,
x2,
x3,
x4,
x5,
x9)
U56_AGA(
x1,
x2,
x3,
x4,
x5,
x6) =
U56_AGA(
x2,
x3,
x4,
x6)
U57_AGA(
x1,
x2,
x3,
x4,
x5,
x6) =
U57_AGA(
x2,
x3,
x4,
x6)
U58_AGA(
x1,
x2,
x3,
x4,
x5,
x6) =
U58_AGA(
x1,
x2,
x3,
x4,
x6)
U59_AGA(
x1,
x2,
x3,
x4,
x5,
x6) =
U59_AGA(
x2,
x3,
x4,
x6)
PL_IN_GAGA(
x1,
x2,
x3,
x4) =
PL_IN_GAGA(
x1,
x3)
U21_GAGA(
x1,
x2,
x3,
x4,
x5) =
U21_GAGA(
x1,
x3,
x5)
U22_GAGA(
x1,
x2,
x3,
x4,
x5) =
U22_GAGA(
x1,
x3,
x5)
U23_GAGA(
x1,
x2,
x3,
x4,
x5) =
U23_GAGA(
x1,
x3,
x5)
U60_AGA(
x1,
x2,
x3,
x4,
x5) =
U60_AGA(
x1,
x2,
x3,
x5)
U61_AGA(
x1,
x2,
x3,
x4,
x5,
x6) =
U61_AGA(
x2,
x3,
x4,
x6)
U62_AGA(
x1,
x2,
x3,
x4,
x5,
x6) =
U62_AGA(
x2,
x3,
x4,
x6)
U63_AGA(
x1,
x2,
x3,
x4,
x5,
x6) =
U63_AGA(
x1,
x2,
x3,
x4,
x6)
U64_AGA(
x1,
x2,
x3,
x4,
x5) =
U64_AGA(
x2,
x3,
x5)
U65_AGA(
x1,
x2,
x3,
x4,
x5,
x6) =
U65_AGA(
x2,
x3,
x4,
x6)
U66_AGA(
x1,
x2,
x3,
x4,
x5,
x6) =
U66_AGA(
x2,
x3,
x4,
x6)
U67_AGA(
x1,
x2,
x3,
x4,
x5,
x6) =
U67_AGA(
x2,
x3,
x4,
x6)
We have to consider all (P,R,Pi)-chains
(7) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LOPSTR] contains 6 SCCs with 97 less nodes.
(8) Complex Obligation (AND)
(9) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
LESSM_IN_GG(s(X1), s(X2)) → LESSM_IN_GG(X1, X2)
The TRS R consists of the following rules:
lesscF_in_ga(0, s(X1)) → lesscF_out_ga(0, s(X1))
lesscF_in_ga(s(X1), s(X2)) → U104_ga(X1, X2, lesscF_in_ga(X1, X2))
U104_ga(X1, X2, lesscF_out_ga(X1, X2)) → lesscF_out_ga(s(X1), s(X2))
lesscA_in_gg(0, s(X1)) → lesscA_out_gg(0, s(X1))
lesscA_in_gg(s(X1), s(X2)) → U69_gg(X1, X2, lesscA_in_gg(X1, X2))
U69_gg(X1, X2, lesscA_out_gg(X1, X2)) → lesscA_out_gg(s(X1), s(X2))
lesscA_in_ag(0, s(X1)) → lesscA_out_ag(0, s(X1))
lesscA_in_ag(s(X1), s(X2)) → U69_ag(X1, X2, lesscA_in_ag(X1, X2))
U69_ag(X1, X2, lesscA_out_ag(X1, X2)) → lesscA_out_ag(s(X1), s(X2))
lesscM_in_gg(0, s(X1)) → lesscM_out_gg(0, s(X1))
lesscM_in_gg(s(X1), s(X2)) → U110_gg(X1, X2, lesscM_in_gg(X1, X2))
U110_gg(X1, X2, lesscM_out_gg(X1, X2)) → lesscM_out_gg(s(X1), s(X2))
The argument filtering Pi contains the following mapping:
s(
x1) =
s(
x1)
lesscF_in_ga(
x1,
x2) =
lesscF_in_ga(
x1)
0 =
0
lesscF_out_ga(
x1,
x2) =
lesscF_out_ga(
x1)
U104_ga(
x1,
x2,
x3) =
U104_ga(
x1,
x3)
lesscA_in_gg(
x1,
x2) =
lesscA_in_gg(
x1,
x2)
lesscA_out_gg(
x1,
x2) =
lesscA_out_gg(
x1,
x2)
U69_gg(
x1,
x2,
x3) =
U69_gg(
x1,
x2,
x3)
lesscA_in_ag(
x1,
x2) =
lesscA_in_ag(
x2)
lesscA_out_ag(
x1,
x2) =
lesscA_out_ag(
x1,
x2)
U69_ag(
x1,
x2,
x3) =
U69_ag(
x2,
x3)
lesscM_in_gg(
x1,
x2) =
lesscM_in_gg(
x1,
x2)
lesscM_out_gg(
x1,
x2) =
lesscM_out_gg(
x1,
x2)
U110_gg(
x1,
x2,
x3) =
U110_gg(
x1,
x2,
x3)
LESSM_IN_GG(
x1,
x2) =
LESSM_IN_GG(
x1,
x2)
We have to consider all (P,R,Pi)-chains
(10) UsableRulesProof (EQUIVALENT transformation)
For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.
(11) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
LESSM_IN_GG(s(X1), s(X2)) → LESSM_IN_GG(X1, X2)
R is empty.
Pi is empty.
We have to consider all (P,R,Pi)-chains
(12) PiDPToQDPProof (EQUIVALENT transformation)
Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.
(13) Obligation:
Q DP problem:
The TRS P consists of the following rules:
LESSM_IN_GG(s(X1), s(X2)) → LESSM_IN_GG(X1, X2)
R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
(14) QDPSizeChangeProof (EQUIVALENT transformation)
By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.
From the DPs we obtained the following set of size-change graphs:
- LESSM_IN_GG(s(X1), s(X2)) → LESSM_IN_GG(X1, X2)
The graph contains the following edges 1 > 1, 2 > 2
(15) YES
(16) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
DELMING_IN_GAA(tree(X1, X2, X3), X4, tree(X1, X5, X6)) → DELMING_IN_GAA(X2, X4, X5)
The TRS R consists of the following rules:
lesscF_in_ga(0, s(X1)) → lesscF_out_ga(0, s(X1))
lesscF_in_ga(s(X1), s(X2)) → U104_ga(X1, X2, lesscF_in_ga(X1, X2))
U104_ga(X1, X2, lesscF_out_ga(X1, X2)) → lesscF_out_ga(s(X1), s(X2))
lesscA_in_gg(0, s(X1)) → lesscA_out_gg(0, s(X1))
lesscA_in_gg(s(X1), s(X2)) → U69_gg(X1, X2, lesscA_in_gg(X1, X2))
U69_gg(X1, X2, lesscA_out_gg(X1, X2)) → lesscA_out_gg(s(X1), s(X2))
lesscA_in_ag(0, s(X1)) → lesscA_out_ag(0, s(X1))
lesscA_in_ag(s(X1), s(X2)) → U69_ag(X1, X2, lesscA_in_ag(X1, X2))
U69_ag(X1, X2, lesscA_out_ag(X1, X2)) → lesscA_out_ag(s(X1), s(X2))
lesscM_in_gg(0, s(X1)) → lesscM_out_gg(0, s(X1))
lesscM_in_gg(s(X1), s(X2)) → U110_gg(X1, X2, lesscM_in_gg(X1, X2))
U110_gg(X1, X2, lesscM_out_gg(X1, X2)) → lesscM_out_gg(s(X1), s(X2))
The argument filtering Pi contains the following mapping:
tree(
x1,
x2,
x3) =
tree(
x1,
x2,
x3)
s(
x1) =
s(
x1)
lesscF_in_ga(
x1,
x2) =
lesscF_in_ga(
x1)
0 =
0
lesscF_out_ga(
x1,
x2) =
lesscF_out_ga(
x1)
U104_ga(
x1,
x2,
x3) =
U104_ga(
x1,
x3)
lesscA_in_gg(
x1,
x2) =
lesscA_in_gg(
x1,
x2)
lesscA_out_gg(
x1,
x2) =
lesscA_out_gg(
x1,
x2)
U69_gg(
x1,
x2,
x3) =
U69_gg(
x1,
x2,
x3)
lesscA_in_ag(
x1,
x2) =
lesscA_in_ag(
x2)
lesscA_out_ag(
x1,
x2) =
lesscA_out_ag(
x1,
x2)
U69_ag(
x1,
x2,
x3) =
U69_ag(
x2,
x3)
lesscM_in_gg(
x1,
x2) =
lesscM_in_gg(
x1,
x2)
lesscM_out_gg(
x1,
x2) =
lesscM_out_gg(
x1,
x2)
U110_gg(
x1,
x2,
x3) =
U110_gg(
x1,
x2,
x3)
DELMING_IN_GAA(
x1,
x2,
x3) =
DELMING_IN_GAA(
x1)
We have to consider all (P,R,Pi)-chains
(17) UsableRulesProof (EQUIVALENT transformation)
For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.
(18) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
DELMING_IN_GAA(tree(X1, X2, X3), X4, tree(X1, X5, X6)) → DELMING_IN_GAA(X2, X4, X5)
R is empty.
The argument filtering Pi contains the following mapping:
tree(
x1,
x2,
x3) =
tree(
x1,
x2,
x3)
DELMING_IN_GAA(
x1,
x2,
x3) =
DELMING_IN_GAA(
x1)
We have to consider all (P,R,Pi)-chains
(19) PiDPToQDPProof (SOUND transformation)
Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.
(20) Obligation:
Q DP problem:
The TRS P consists of the following rules:
DELMING_IN_GAA(tree(X1, X2, X3)) → DELMING_IN_GAA(X2)
R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
(21) QDPSizeChangeProof (EQUIVALENT transformation)
By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.
From the DPs we obtained the following set of size-change graphs:
- DELMING_IN_GAA(tree(X1, X2, X3)) → DELMING_IN_GAA(X2)
The graph contains the following edges 1 > 1
(22) YES
(23) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
DELETEK_IN_GGA(X1, tree(X2, X3, X4), tree(X2, X5, X4)) → PI_IN_GGGA(X1, X2, X3, X5)
PI_IN_GGGA(X1, X2, X3, X4) → U13_GGGA(X1, X2, X3, X4, lesscM_in_gg(X1, X2))
U13_GGGA(X1, X2, X3, X4, lesscM_out_gg(X1, X2)) → DELETEK_IN_GGA(X1, X3, X4)
DELETEK_IN_GGA(X1, tree(X2, X3, X4), tree(X2, X3, X5)) → PJ_IN_GGGA(X2, X1, X4, X5)
PJ_IN_GGGA(X1, X2, X3, X4) → U19_GGGA(X1, X2, X3, X4, lesscM_in_gg(X1, X2))
U19_GGGA(X1, X2, X3, X4, lesscM_out_gg(X1, X2)) → DELETEK_IN_GGA(X2, X3, X4)
The TRS R consists of the following rules:
lesscF_in_ga(0, s(X1)) → lesscF_out_ga(0, s(X1))
lesscF_in_ga(s(X1), s(X2)) → U104_ga(X1, X2, lesscF_in_ga(X1, X2))
U104_ga(X1, X2, lesscF_out_ga(X1, X2)) → lesscF_out_ga(s(X1), s(X2))
lesscA_in_gg(0, s(X1)) → lesscA_out_gg(0, s(X1))
lesscA_in_gg(s(X1), s(X2)) → U69_gg(X1, X2, lesscA_in_gg(X1, X2))
U69_gg(X1, X2, lesscA_out_gg(X1, X2)) → lesscA_out_gg(s(X1), s(X2))
lesscA_in_ag(0, s(X1)) → lesscA_out_ag(0, s(X1))
lesscA_in_ag(s(X1), s(X2)) → U69_ag(X1, X2, lesscA_in_ag(X1, X2))
U69_ag(X1, X2, lesscA_out_ag(X1, X2)) → lesscA_out_ag(s(X1), s(X2))
lesscM_in_gg(0, s(X1)) → lesscM_out_gg(0, s(X1))
lesscM_in_gg(s(X1), s(X2)) → U110_gg(X1, X2, lesscM_in_gg(X1, X2))
U110_gg(X1, X2, lesscM_out_gg(X1, X2)) → lesscM_out_gg(s(X1), s(X2))
The argument filtering Pi contains the following mapping:
tree(
x1,
x2,
x3) =
tree(
x1,
x2,
x3)
s(
x1) =
s(
x1)
lesscF_in_ga(
x1,
x2) =
lesscF_in_ga(
x1)
0 =
0
lesscF_out_ga(
x1,
x2) =
lesscF_out_ga(
x1)
U104_ga(
x1,
x2,
x3) =
U104_ga(
x1,
x3)
lesscA_in_gg(
x1,
x2) =
lesscA_in_gg(
x1,
x2)
lesscA_out_gg(
x1,
x2) =
lesscA_out_gg(
x1,
x2)
U69_gg(
x1,
x2,
x3) =
U69_gg(
x1,
x2,
x3)
lesscA_in_ag(
x1,
x2) =
lesscA_in_ag(
x2)
lesscA_out_ag(
x1,
x2) =
lesscA_out_ag(
x1,
x2)
U69_ag(
x1,
x2,
x3) =
U69_ag(
x2,
x3)
lesscM_in_gg(
x1,
x2) =
lesscM_in_gg(
x1,
x2)
lesscM_out_gg(
x1,
x2) =
lesscM_out_gg(
x1,
x2)
U110_gg(
x1,
x2,
x3) =
U110_gg(
x1,
x2,
x3)
PI_IN_GGGA(
x1,
x2,
x3,
x4) =
PI_IN_GGGA(
x1,
x2,
x3)
U13_GGGA(
x1,
x2,
x3,
x4,
x5) =
U13_GGGA(
x1,
x2,
x3,
x5)
DELETEK_IN_GGA(
x1,
x2,
x3) =
DELETEK_IN_GGA(
x1,
x2)
PJ_IN_GGGA(
x1,
x2,
x3,
x4) =
PJ_IN_GGGA(
x1,
x2,
x3)
U19_GGGA(
x1,
x2,
x3,
x4,
x5) =
U19_GGGA(
x1,
x2,
x3,
x5)
We have to consider all (P,R,Pi)-chains
(24) UsableRulesProof (EQUIVALENT transformation)
For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.
(25) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
DELETEK_IN_GGA(X1, tree(X2, X3, X4), tree(X2, X5, X4)) → PI_IN_GGGA(X1, X2, X3, X5)
PI_IN_GGGA(X1, X2, X3, X4) → U13_GGGA(X1, X2, X3, X4, lesscM_in_gg(X1, X2))
U13_GGGA(X1, X2, X3, X4, lesscM_out_gg(X1, X2)) → DELETEK_IN_GGA(X1, X3, X4)
DELETEK_IN_GGA(X1, tree(X2, X3, X4), tree(X2, X3, X5)) → PJ_IN_GGGA(X2, X1, X4, X5)
PJ_IN_GGGA(X1, X2, X3, X4) → U19_GGGA(X1, X2, X3, X4, lesscM_in_gg(X1, X2))
U19_GGGA(X1, X2, X3, X4, lesscM_out_gg(X1, X2)) → DELETEK_IN_GGA(X2, X3, X4)
The TRS R consists of the following rules:
lesscM_in_gg(0, s(X1)) → lesscM_out_gg(0, s(X1))
lesscM_in_gg(s(X1), s(X2)) → U110_gg(X1, X2, lesscM_in_gg(X1, X2))
U110_gg(X1, X2, lesscM_out_gg(X1, X2)) → lesscM_out_gg(s(X1), s(X2))
The argument filtering Pi contains the following mapping:
tree(
x1,
x2,
x3) =
tree(
x1,
x2,
x3)
s(
x1) =
s(
x1)
0 =
0
lesscM_in_gg(
x1,
x2) =
lesscM_in_gg(
x1,
x2)
lesscM_out_gg(
x1,
x2) =
lesscM_out_gg(
x1,
x2)
U110_gg(
x1,
x2,
x3) =
U110_gg(
x1,
x2,
x3)
PI_IN_GGGA(
x1,
x2,
x3,
x4) =
PI_IN_GGGA(
x1,
x2,
x3)
U13_GGGA(
x1,
x2,
x3,
x4,
x5) =
U13_GGGA(
x1,
x2,
x3,
x5)
DELETEK_IN_GGA(
x1,
x2,
x3) =
DELETEK_IN_GGA(
x1,
x2)
PJ_IN_GGGA(
x1,
x2,
x3,
x4) =
PJ_IN_GGGA(
x1,
x2,
x3)
U19_GGGA(
x1,
x2,
x3,
x4,
x5) =
U19_GGGA(
x1,
x2,
x3,
x5)
We have to consider all (P,R,Pi)-chains
(26) PiDPToQDPProof (SOUND transformation)
Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.
(27) Obligation:
Q DP problem:
The TRS P consists of the following rules:
DELETEK_IN_GGA(X1, tree(X2, X3, X4)) → PI_IN_GGGA(X1, X2, X3)
PI_IN_GGGA(X1, X2, X3) → U13_GGGA(X1, X2, X3, lesscM_in_gg(X1, X2))
U13_GGGA(X1, X2, X3, lesscM_out_gg(X1, X2)) → DELETEK_IN_GGA(X1, X3)
DELETEK_IN_GGA(X1, tree(X2, X3, X4)) → PJ_IN_GGGA(X2, X1, X4)
PJ_IN_GGGA(X1, X2, X3) → U19_GGGA(X1, X2, X3, lesscM_in_gg(X1, X2))
U19_GGGA(X1, X2, X3, lesscM_out_gg(X1, X2)) → DELETEK_IN_GGA(X2, X3)
The TRS R consists of the following rules:
lesscM_in_gg(0, s(X1)) → lesscM_out_gg(0, s(X1))
lesscM_in_gg(s(X1), s(X2)) → U110_gg(X1, X2, lesscM_in_gg(X1, X2))
U110_gg(X1, X2, lesscM_out_gg(X1, X2)) → lesscM_out_gg(s(X1), s(X2))
The set Q consists of the following terms:
lesscM_in_gg(x0, x1)
U110_gg(x0, x1, x2)
We have to consider all (P,Q,R)-chains.
(28) QDPSizeChangeProof (EQUIVALENT transformation)
By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.
From the DPs we obtained the following set of size-change graphs:
- PI_IN_GGGA(X1, X2, X3) → U13_GGGA(X1, X2, X3, lesscM_in_gg(X1, X2))
The graph contains the following edges 1 >= 1, 2 >= 2, 3 >= 3
- U13_GGGA(X1, X2, X3, lesscM_out_gg(X1, X2)) → DELETEK_IN_GGA(X1, X3)
The graph contains the following edges 1 >= 1, 4 > 1, 3 >= 2
- U19_GGGA(X1, X2, X3, lesscM_out_gg(X1, X2)) → DELETEK_IN_GGA(X2, X3)
The graph contains the following edges 2 >= 1, 4 > 1, 3 >= 2
- DELETEK_IN_GGA(X1, tree(X2, X3, X4)) → PI_IN_GGGA(X1, X2, X3)
The graph contains the following edges 1 >= 1, 2 > 2, 2 > 3
- DELETEK_IN_GGA(X1, tree(X2, X3, X4)) → PJ_IN_GGGA(X2, X1, X4)
The graph contains the following edges 2 > 1, 1 >= 2, 2 > 3
- PJ_IN_GGGA(X1, X2, X3) → U19_GGGA(X1, X2, X3, lesscM_in_gg(X1, X2))
The graph contains the following edges 1 >= 1, 2 >= 2, 3 >= 3
(29) YES
(30) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
LESSF_IN_GA(s(X1), s(X2)) → LESSF_IN_GA(X1, X2)
The TRS R consists of the following rules:
lesscF_in_ga(0, s(X1)) → lesscF_out_ga(0, s(X1))
lesscF_in_ga(s(X1), s(X2)) → U104_ga(X1, X2, lesscF_in_ga(X1, X2))
U104_ga(X1, X2, lesscF_out_ga(X1, X2)) → lesscF_out_ga(s(X1), s(X2))
lesscA_in_gg(0, s(X1)) → lesscA_out_gg(0, s(X1))
lesscA_in_gg(s(X1), s(X2)) → U69_gg(X1, X2, lesscA_in_gg(X1, X2))
U69_gg(X1, X2, lesscA_out_gg(X1, X2)) → lesscA_out_gg(s(X1), s(X2))
lesscA_in_ag(0, s(X1)) → lesscA_out_ag(0, s(X1))
lesscA_in_ag(s(X1), s(X2)) → U69_ag(X1, X2, lesscA_in_ag(X1, X2))
U69_ag(X1, X2, lesscA_out_ag(X1, X2)) → lesscA_out_ag(s(X1), s(X2))
lesscM_in_gg(0, s(X1)) → lesscM_out_gg(0, s(X1))
lesscM_in_gg(s(X1), s(X2)) → U110_gg(X1, X2, lesscM_in_gg(X1, X2))
U110_gg(X1, X2, lesscM_out_gg(X1, X2)) → lesscM_out_gg(s(X1), s(X2))
The argument filtering Pi contains the following mapping:
s(
x1) =
s(
x1)
lesscF_in_ga(
x1,
x2) =
lesscF_in_ga(
x1)
0 =
0
lesscF_out_ga(
x1,
x2) =
lesscF_out_ga(
x1)
U104_ga(
x1,
x2,
x3) =
U104_ga(
x1,
x3)
lesscA_in_gg(
x1,
x2) =
lesscA_in_gg(
x1,
x2)
lesscA_out_gg(
x1,
x2) =
lesscA_out_gg(
x1,
x2)
U69_gg(
x1,
x2,
x3) =
U69_gg(
x1,
x2,
x3)
lesscA_in_ag(
x1,
x2) =
lesscA_in_ag(
x2)
lesscA_out_ag(
x1,
x2) =
lesscA_out_ag(
x1,
x2)
U69_ag(
x1,
x2,
x3) =
U69_ag(
x2,
x3)
lesscM_in_gg(
x1,
x2) =
lesscM_in_gg(
x1,
x2)
lesscM_out_gg(
x1,
x2) =
lesscM_out_gg(
x1,
x2)
U110_gg(
x1,
x2,
x3) =
U110_gg(
x1,
x2,
x3)
LESSF_IN_GA(
x1,
x2) =
LESSF_IN_GA(
x1)
We have to consider all (P,R,Pi)-chains
(31) UsableRulesProof (EQUIVALENT transformation)
For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.
(32) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
LESSF_IN_GA(s(X1), s(X2)) → LESSF_IN_GA(X1, X2)
R is empty.
The argument filtering Pi contains the following mapping:
s(
x1) =
s(
x1)
LESSF_IN_GA(
x1,
x2) =
LESSF_IN_GA(
x1)
We have to consider all (P,R,Pi)-chains
(33) PiDPToQDPProof (SOUND transformation)
Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.
(34) Obligation:
Q DP problem:
The TRS P consists of the following rules:
LESSF_IN_GA(s(X1)) → LESSF_IN_GA(X1)
R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
(35) QDPSizeChangeProof (EQUIVALENT transformation)
By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.
From the DPs we obtained the following set of size-change graphs:
- LESSF_IN_GA(s(X1)) → LESSF_IN_GA(X1)
The graph contains the following edges 1 > 1
(36) YES
(37) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
LESSA_IN_AG(s(X1), s(X2)) → LESSA_IN_AG(X1, X2)
The TRS R consists of the following rules:
lesscF_in_ga(0, s(X1)) → lesscF_out_ga(0, s(X1))
lesscF_in_ga(s(X1), s(X2)) → U104_ga(X1, X2, lesscF_in_ga(X1, X2))
U104_ga(X1, X2, lesscF_out_ga(X1, X2)) → lesscF_out_ga(s(X1), s(X2))
lesscA_in_gg(0, s(X1)) → lesscA_out_gg(0, s(X1))
lesscA_in_gg(s(X1), s(X2)) → U69_gg(X1, X2, lesscA_in_gg(X1, X2))
U69_gg(X1, X2, lesscA_out_gg(X1, X2)) → lesscA_out_gg(s(X1), s(X2))
lesscA_in_ag(0, s(X1)) → lesscA_out_ag(0, s(X1))
lesscA_in_ag(s(X1), s(X2)) → U69_ag(X1, X2, lesscA_in_ag(X1, X2))
U69_ag(X1, X2, lesscA_out_ag(X1, X2)) → lesscA_out_ag(s(X1), s(X2))
lesscM_in_gg(0, s(X1)) → lesscM_out_gg(0, s(X1))
lesscM_in_gg(s(X1), s(X2)) → U110_gg(X1, X2, lesscM_in_gg(X1, X2))
U110_gg(X1, X2, lesscM_out_gg(X1, X2)) → lesscM_out_gg(s(X1), s(X2))
The argument filtering Pi contains the following mapping:
s(
x1) =
s(
x1)
lesscF_in_ga(
x1,
x2) =
lesscF_in_ga(
x1)
0 =
0
lesscF_out_ga(
x1,
x2) =
lesscF_out_ga(
x1)
U104_ga(
x1,
x2,
x3) =
U104_ga(
x1,
x3)
lesscA_in_gg(
x1,
x2) =
lesscA_in_gg(
x1,
x2)
lesscA_out_gg(
x1,
x2) =
lesscA_out_gg(
x1,
x2)
U69_gg(
x1,
x2,
x3) =
U69_gg(
x1,
x2,
x3)
lesscA_in_ag(
x1,
x2) =
lesscA_in_ag(
x2)
lesscA_out_ag(
x1,
x2) =
lesscA_out_ag(
x1,
x2)
U69_ag(
x1,
x2,
x3) =
U69_ag(
x2,
x3)
lesscM_in_gg(
x1,
x2) =
lesscM_in_gg(
x1,
x2)
lesscM_out_gg(
x1,
x2) =
lesscM_out_gg(
x1,
x2)
U110_gg(
x1,
x2,
x3) =
U110_gg(
x1,
x2,
x3)
LESSA_IN_AG(
x1,
x2) =
LESSA_IN_AG(
x2)
We have to consider all (P,R,Pi)-chains
(38) UsableRulesProof (EQUIVALENT transformation)
For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.
(39) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
LESSA_IN_AG(s(X1), s(X2)) → LESSA_IN_AG(X1, X2)
R is empty.
The argument filtering Pi contains the following mapping:
s(
x1) =
s(
x1)
LESSA_IN_AG(
x1,
x2) =
LESSA_IN_AG(
x2)
We have to consider all (P,R,Pi)-chains
(40) PiDPToQDPProof (SOUND transformation)
Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.
(41) Obligation:
Q DP problem:
The TRS P consists of the following rules:
LESSA_IN_AG(s(X2)) → LESSA_IN_AG(X2)
R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
(42) QDPSizeChangeProof (EQUIVALENT transformation)
By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.
From the DPs we obtained the following set of size-change graphs:
- LESSA_IN_AG(s(X2)) → LESSA_IN_AG(X2)
The graph contains the following edges 1 > 1
(43) YES
(44) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
DELETEB_IN_AGA(X1, tree(X2, void, X3), tree(X2, void, X4)) → PH_IN_GAGA(X2, X1, X3, X4)
PH_IN_GAGA(X1, X2, X3, X4) → U9_GAGA(X1, X2, X3, X4, lesscF_in_ga(X1, X2))
U9_GAGA(X1, X2, X3, X4, lesscF_out_ga(X1, X2)) → DELETEB_IN_AGA(X2, X3, X4)
DELETEB_IN_AGA(s(X1), tree(0, void, X2), tree(0, void, X3)) → DELETEB_IN_AGA(s(X1), X2, X3)
DELETEB_IN_AGA(s(X1), tree(s(X2), void, X3), tree(s(X2), void, X4)) → U37_AGA(X1, X2, X3, X4, lesscF_in_ga(X2, X1))
U37_AGA(X1, X2, X3, X4, lesscF_out_ga(X2, X1)) → DELETEB_IN_AGA(s(X1), X3, X4)
DELETEB_IN_AGA(X1, tree(X2, X3, X4), tree(X2, X3, X5)) → PL_IN_GAGA(X2, X1, X4, X5)
PL_IN_GAGA(X1, X2, X3, X4) → U22_GAGA(X1, X2, X3, X4, lesscF_in_ga(X1, X2))
U22_GAGA(X1, X2, X3, X4, lesscF_out_ga(X1, X2)) → DELETEB_IN_AGA(X2, X3, X4)
DELETEB_IN_AGA(s(X1), tree(0, X2, X3), tree(0, X2, X4)) → DELETEB_IN_AGA(s(X1), X3, X4)
DELETEB_IN_AGA(s(X1), tree(s(X2), X3, X4), tree(s(X2), X3, X5)) → U66_AGA(X1, X2, X3, X4, X5, lesscF_in_ga(X2, X1))
U66_AGA(X1, X2, X3, X4, X5, lesscF_out_ga(X2, X1)) → DELETEB_IN_AGA(s(X1), X4, X5)
The TRS R consists of the following rules:
lesscF_in_ga(0, s(X1)) → lesscF_out_ga(0, s(X1))
lesscF_in_ga(s(X1), s(X2)) → U104_ga(X1, X2, lesscF_in_ga(X1, X2))
U104_ga(X1, X2, lesscF_out_ga(X1, X2)) → lesscF_out_ga(s(X1), s(X2))
lesscA_in_gg(0, s(X1)) → lesscA_out_gg(0, s(X1))
lesscA_in_gg(s(X1), s(X2)) → U69_gg(X1, X2, lesscA_in_gg(X1, X2))
U69_gg(X1, X2, lesscA_out_gg(X1, X2)) → lesscA_out_gg(s(X1), s(X2))
lesscA_in_ag(0, s(X1)) → lesscA_out_ag(0, s(X1))
lesscA_in_ag(s(X1), s(X2)) → U69_ag(X1, X2, lesscA_in_ag(X1, X2))
U69_ag(X1, X2, lesscA_out_ag(X1, X2)) → lesscA_out_ag(s(X1), s(X2))
lesscM_in_gg(0, s(X1)) → lesscM_out_gg(0, s(X1))
lesscM_in_gg(s(X1), s(X2)) → U110_gg(X1, X2, lesscM_in_gg(X1, X2))
U110_gg(X1, X2, lesscM_out_gg(X1, X2)) → lesscM_out_gg(s(X1), s(X2))
The argument filtering Pi contains the following mapping:
tree(
x1,
x2,
x3) =
tree(
x1,
x2,
x3)
void =
void
s(
x1) =
s(
x1)
lesscF_in_ga(
x1,
x2) =
lesscF_in_ga(
x1)
0 =
0
lesscF_out_ga(
x1,
x2) =
lesscF_out_ga(
x1)
U104_ga(
x1,
x2,
x3) =
U104_ga(
x1,
x3)
lesscA_in_gg(
x1,
x2) =
lesscA_in_gg(
x1,
x2)
lesscA_out_gg(
x1,
x2) =
lesscA_out_gg(
x1,
x2)
U69_gg(
x1,
x2,
x3) =
U69_gg(
x1,
x2,
x3)
lesscA_in_ag(
x1,
x2) =
lesscA_in_ag(
x2)
lesscA_out_ag(
x1,
x2) =
lesscA_out_ag(
x1,
x2)
U69_ag(
x1,
x2,
x3) =
U69_ag(
x2,
x3)
lesscM_in_gg(
x1,
x2) =
lesscM_in_gg(
x1,
x2)
lesscM_out_gg(
x1,
x2) =
lesscM_out_gg(
x1,
x2)
U110_gg(
x1,
x2,
x3) =
U110_gg(
x1,
x2,
x3)
DELETEB_IN_AGA(
x1,
x2,
x3) =
DELETEB_IN_AGA(
x2)
PH_IN_GAGA(
x1,
x2,
x3,
x4) =
PH_IN_GAGA(
x1,
x3)
U9_GAGA(
x1,
x2,
x3,
x4,
x5) =
U9_GAGA(
x1,
x3,
x5)
U37_AGA(
x1,
x2,
x3,
x4,
x5) =
U37_AGA(
x2,
x3,
x5)
PL_IN_GAGA(
x1,
x2,
x3,
x4) =
PL_IN_GAGA(
x1,
x3)
U22_GAGA(
x1,
x2,
x3,
x4,
x5) =
U22_GAGA(
x1,
x3,
x5)
U66_AGA(
x1,
x2,
x3,
x4,
x5,
x6) =
U66_AGA(
x2,
x3,
x4,
x6)
We have to consider all (P,R,Pi)-chains
(45) UsableRulesProof (EQUIVALENT transformation)
For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.
(46) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
DELETEB_IN_AGA(X1, tree(X2, void, X3), tree(X2, void, X4)) → PH_IN_GAGA(X2, X1, X3, X4)
PH_IN_GAGA(X1, X2, X3, X4) → U9_GAGA(X1, X2, X3, X4, lesscF_in_ga(X1, X2))
U9_GAGA(X1, X2, X3, X4, lesscF_out_ga(X1, X2)) → DELETEB_IN_AGA(X2, X3, X4)
DELETEB_IN_AGA(s(X1), tree(0, void, X2), tree(0, void, X3)) → DELETEB_IN_AGA(s(X1), X2, X3)
DELETEB_IN_AGA(s(X1), tree(s(X2), void, X3), tree(s(X2), void, X4)) → U37_AGA(X1, X2, X3, X4, lesscF_in_ga(X2, X1))
U37_AGA(X1, X2, X3, X4, lesscF_out_ga(X2, X1)) → DELETEB_IN_AGA(s(X1), X3, X4)
DELETEB_IN_AGA(X1, tree(X2, X3, X4), tree(X2, X3, X5)) → PL_IN_GAGA(X2, X1, X4, X5)
PL_IN_GAGA(X1, X2, X3, X4) → U22_GAGA(X1, X2, X3, X4, lesscF_in_ga(X1, X2))
U22_GAGA(X1, X2, X3, X4, lesscF_out_ga(X1, X2)) → DELETEB_IN_AGA(X2, X3, X4)
DELETEB_IN_AGA(s(X1), tree(0, X2, X3), tree(0, X2, X4)) → DELETEB_IN_AGA(s(X1), X3, X4)
DELETEB_IN_AGA(s(X1), tree(s(X2), X3, X4), tree(s(X2), X3, X5)) → U66_AGA(X1, X2, X3, X4, X5, lesscF_in_ga(X2, X1))
U66_AGA(X1, X2, X3, X4, X5, lesscF_out_ga(X2, X1)) → DELETEB_IN_AGA(s(X1), X4, X5)
The TRS R consists of the following rules:
lesscF_in_ga(0, s(X1)) → lesscF_out_ga(0, s(X1))
lesscF_in_ga(s(X1), s(X2)) → U104_ga(X1, X2, lesscF_in_ga(X1, X2))
U104_ga(X1, X2, lesscF_out_ga(X1, X2)) → lesscF_out_ga(s(X1), s(X2))
The argument filtering Pi contains the following mapping:
tree(
x1,
x2,
x3) =
tree(
x1,
x2,
x3)
void =
void
s(
x1) =
s(
x1)
lesscF_in_ga(
x1,
x2) =
lesscF_in_ga(
x1)
0 =
0
lesscF_out_ga(
x1,
x2) =
lesscF_out_ga(
x1)
U104_ga(
x1,
x2,
x3) =
U104_ga(
x1,
x3)
DELETEB_IN_AGA(
x1,
x2,
x3) =
DELETEB_IN_AGA(
x2)
PH_IN_GAGA(
x1,
x2,
x3,
x4) =
PH_IN_GAGA(
x1,
x3)
U9_GAGA(
x1,
x2,
x3,
x4,
x5) =
U9_GAGA(
x1,
x3,
x5)
U37_AGA(
x1,
x2,
x3,
x4,
x5) =
U37_AGA(
x2,
x3,
x5)
PL_IN_GAGA(
x1,
x2,
x3,
x4) =
PL_IN_GAGA(
x1,
x3)
U22_GAGA(
x1,
x2,
x3,
x4,
x5) =
U22_GAGA(
x1,
x3,
x5)
U66_AGA(
x1,
x2,
x3,
x4,
x5,
x6) =
U66_AGA(
x2,
x3,
x4,
x6)
We have to consider all (P,R,Pi)-chains
(47) PiDPToQDPProof (SOUND transformation)
Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.
(48) Obligation:
Q DP problem:
The TRS P consists of the following rules:
DELETEB_IN_AGA(tree(X2, void, X3)) → PH_IN_GAGA(X2, X3)
PH_IN_GAGA(X1, X3) → U9_GAGA(X1, X3, lesscF_in_ga(X1))
U9_GAGA(X1, X3, lesscF_out_ga(X1)) → DELETEB_IN_AGA(X3)
DELETEB_IN_AGA(tree(0, void, X2)) → DELETEB_IN_AGA(X2)
DELETEB_IN_AGA(tree(s(X2), void, X3)) → U37_AGA(X2, X3, lesscF_in_ga(X2))
U37_AGA(X2, X3, lesscF_out_ga(X2)) → DELETEB_IN_AGA(X3)
DELETEB_IN_AGA(tree(X2, X3, X4)) → PL_IN_GAGA(X2, X4)
PL_IN_GAGA(X1, X3) → U22_GAGA(X1, X3, lesscF_in_ga(X1))
U22_GAGA(X1, X3, lesscF_out_ga(X1)) → DELETEB_IN_AGA(X3)
DELETEB_IN_AGA(tree(0, X2, X3)) → DELETEB_IN_AGA(X3)
DELETEB_IN_AGA(tree(s(X2), X3, X4)) → U66_AGA(X2, X3, X4, lesscF_in_ga(X2))
U66_AGA(X2, X3, X4, lesscF_out_ga(X2)) → DELETEB_IN_AGA(X4)
The TRS R consists of the following rules:
lesscF_in_ga(0) → lesscF_out_ga(0)
lesscF_in_ga(s(X1)) → U104_ga(X1, lesscF_in_ga(X1))
U104_ga(X1, lesscF_out_ga(X1)) → lesscF_out_ga(s(X1))
The set Q consists of the following terms:
lesscF_in_ga(x0)
U104_ga(x0, x1)
We have to consider all (P,Q,R)-chains.
(49) QDPSizeChangeProof (EQUIVALENT transformation)
By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.
From the DPs we obtained the following set of size-change graphs:
- PH_IN_GAGA(X1, X3) → U9_GAGA(X1, X3, lesscF_in_ga(X1))
The graph contains the following edges 1 >= 1, 2 >= 2
- U9_GAGA(X1, X3, lesscF_out_ga(X1)) → DELETEB_IN_AGA(X3)
The graph contains the following edges 2 >= 1
- DELETEB_IN_AGA(tree(X2, void, X3)) → PH_IN_GAGA(X2, X3)
The graph contains the following edges 1 > 1, 1 > 2
- PL_IN_GAGA(X1, X3) → U22_GAGA(X1, X3, lesscF_in_ga(X1))
The graph contains the following edges 1 >= 1, 2 >= 2
- U37_AGA(X2, X3, lesscF_out_ga(X2)) → DELETEB_IN_AGA(X3)
The graph contains the following edges 2 >= 1
- DELETEB_IN_AGA(tree(s(X2), void, X3)) → U37_AGA(X2, X3, lesscF_in_ga(X2))
The graph contains the following edges 1 > 1, 1 > 2
- U22_GAGA(X1, X3, lesscF_out_ga(X1)) → DELETEB_IN_AGA(X3)
The graph contains the following edges 2 >= 1
- U66_AGA(X2, X3, X4, lesscF_out_ga(X2)) → DELETEB_IN_AGA(X4)
The graph contains the following edges 3 >= 1
- DELETEB_IN_AGA(tree(X2, X3, X4)) → PL_IN_GAGA(X2, X4)
The graph contains the following edges 1 > 1, 1 > 2
- DELETEB_IN_AGA(tree(s(X2), X3, X4)) → U66_AGA(X2, X3, X4, lesscF_in_ga(X2))
The graph contains the following edges 1 > 1, 1 > 2, 1 > 3
- DELETEB_IN_AGA(tree(0, void, X2)) → DELETEB_IN_AGA(X2)
The graph contains the following edges 1 > 1
- DELETEB_IN_AGA(tree(0, X2, X3)) → DELETEB_IN_AGA(X3)
The graph contains the following edges 1 > 1
(50) YES